Theorem cbvxabs | index | src |

theorem cbvxabs (A: set) {x y: nat} (B: set x):
  $ X\ x e. A, B == X\ y e. A, (S[y / x] B) $;
StepHypRefExpression
1 eleq2
S[fst z / x] B == S[fst z / y] S[y / x] B -> (snd z e. S[fst z / x] B <-> snd z e. S[fst z / y] S[y / x] B)
2 eqscom
S[fst z / y] S[y / x] B == S[fst z / x] B -> S[fst z / x] B == S[fst z / y] S[y / x] B
3 sbsco
S[fst z / y] S[y / x] B == S[fst z / x] B
4 2, 3 ax_mp
S[fst z / x] B == S[fst z / y] S[y / x] B
5 1, 4 ax_mp
snd z e. S[fst z / x] B <-> snd z e. S[fst z / y] S[y / x] B
6 5 aneq2i
fst z e. A /\ snd z e. S[fst z / x] B <-> fst z e. A /\ snd z e. S[fst z / y] S[y / x] B
7 6 abeqi
{z | fst z e. A /\ snd z e. S[fst z / x] B} == {z | fst z e. A /\ snd z e. S[fst z / y] S[y / x] B}
8 7 conv xab
X\ x e. A, B == X\ y e. A, (S[y / 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)