Theorem sabeq | index | src |

theorem sabeq {x: nat} (A B: set x): $ A. x A == B -> S\ x, A == S\ x, B $;
StepHypRefExpression
1 nfsbs1
FS/ x S[fst a1 / x] A
2 nfsbs1
FS/ x S[fst a1 / x] B
3 1, 2 nfeqs
F/ x S[fst a1 / x] A == S[fst a1 / x] B
4 sbsq
x = fst a1 -> A == S[fst a1 / x] A
5 sbsq
x = fst a1 -> B == S[fst a1 / x] B
6 4, 5 eqseqd
x = fst a1 -> (A == B <-> S[fst a1 / x] A == S[fst a1 / x] B)
7 3, 6 ealeh
A. x A == B -> S[fst a1 / x] A == S[fst a1 / x] B
8 7 eleq2d
A. x A == B -> (snd a1 e. S[fst a1 / x] A <-> snd a1 e. S[fst a1 / x] B)
9 8 abeqd
A. x A == B -> {a1 | snd a1 e. S[fst a1 / x] A} == {a1 | snd a1 e. S[fst a1 / x] B}
10 9 conv sab
A. x A == B -> S\ x, A == S\ x, B

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8)