对公式A和集合变元x,y，若x=y，则将公式A中的z替换为x得到的公式与将公式A中的z替换为y得到的公式等价。
theorem eqs_to_sb_same_iff {z: set} (x y: set) (A: wff z):
$ x = y \imp (\sb x z A \iff \sb y z A) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | _nf_abs | \nf t x = y |
|
| 2 | iff_intror_imp | (t = x \iff t = y) \imp (t = x \imp \fo z (z = t \imp A) \iff t = y \imp \fo z (z = t \imp A)) |
|
| 3 | 2 | _hyp_null_complete | x = y \imp (t = x \iff t = y) \imp (t = x \imp \fo z (z = t \imp A) \iff t = y \imp \fo z (z = t \imp A)) |
| 4 | eqs_repr | x = y \imp (t = x \iff t = y) |
|
| 5 | 4 | _hyp_null_complete | x = y \imp x = y \imp (t = x \iff t = y) |
| 6 | _hyp_null_intro | x = y \imp x = y |
|
| 7 | 5, 6 | _hyp_mp | x = y \imp (t = x \iff t = y) |
| 8 | 3, 7 | _hyp_mp | x = y \imp (t = x \imp \fo z (z = t \imp A) \iff t = y \imp \fo z (z = t \imp A)) |
| 9 | 1, 8 | _hyp_iff_intro_fo | x = y \imp (\fo t (t = x \imp \fo z (z = t \imp A)) \iff \fo t (t = y \imp \fo z (z = t \imp A))) |
| 10 | 9 | conv sb | x = y \imp (\sb x z A \iff \sb y z A) |