Theorem cbvsabs | index | src |

theorem cbvsabs {x y: nat} (A: set x): $ S\ x, A == S\ y, (S[y / x] A) $;
StepHypRefExpression
1 eleq2
S[fst z / x] A == S[fst z / y] S[y / x] A -> (snd z e. S[fst z / x] A <-> snd z e. S[fst z / y] S[y / x] A)
2 eqscom
S[fst z / y] S[y / x] A == S[fst z / x] A -> S[fst z / x] A == S[fst z / y] S[y / x] A
3 sbsco
S[fst z / y] S[y / x] A == S[fst z / x] A
4 2, 3 ax_mp
S[fst z / x] A == S[fst z / y] S[y / x] A
5 1, 4 ax_mp
snd z e. S[fst z / x] A <-> snd z e. S[fst z / y] S[y / x] A
6 5 abeqi
{z | snd z e. S[fst z / x] A} == {z | snd z e. S[fst z / y] S[y / x] A}
7 6 conv sab
S\ x, A == S\ y, (S[y / x] A)

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)