Theorem abeq | index | src |

theorem abeq {x: nat} (p q: wff x): $ A. x (p <-> q) -> {x | p} == {x | q} $;
StepHypRefExpression
1 elab
y e. {x | p} <-> [y / x] p
2 elab
y e. {x | q} <-> [y / x] q
3 nfsb1
F/ x [y / x] p
4 nfsb1
F/ x [y / x] q
5 3, 4 nfbi
F/ x [y / x] p <-> [y / x] q
6 sbq
x = y -> (p <-> [y / x] p)
7 sbq
x = y -> (q <-> [y / x] q)
8 6, 7 bieqd
x = y -> (p <-> q <-> ([y / x] p <-> [y / x] q))
9 5, 8 ealeh
A. x (p <-> q) -> ([y / x] p <-> [y / x] q)
10 1, 2, 9 bitr4g
A. x (p <-> q) -> (y e. {x | p} <-> y e. {x | q})
11 10 iald
A. x (p <-> q) -> A. y (y e. {x | p} <-> y e. {x | q})
12 11 conv eqs
A. x (p <-> q) -> {x | p} == {x | q}

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)