Theorem ellamimaab ≪ | index | src | ≫ 

theorem ellamimaab (a: nat) {x: nat} (v: nat x) (p: wff x):
  $ a e. (\ x, v) '' {x | p} <-> E. x (p /\ a = v) $;
StepHypRefExpression
1 bitr 
(a e. (\ x, v) '' {x | p} <-> a e. (\ y, N[y / x] v) '' {x | p}) ->
  (a e. (\ y, N[y / x] v) '' {x | p} <-> E. x (p /\ a = v)) ->
  (a e. (\ x, v) '' {x | p} <-> E. x (p /\ a = v))
2 eleq2 
(\ x, v) '' {x | p} == (\ y, N[y / x] v) '' {x | p} -> (a e. (\ x, v) '' {x | p} <-> a e. (\ y, N[y / x] v) '' {x | p})
3 imaeq1 
\ x, v == \ y, N[y / x] v -> (\ x, v) '' {x | p} == (\ y, N[y / x] v) '' {x | p}
4 cbvlams 
\ x, v == \ y, N[y / x] v
5 3, 4 ax_mp 
(\ x, v) '' {x | p} == (\ y, N[y / x] v) '' {x | p}
6 2, 5 ax_mp 
a e. (\ x, v) '' {x | p} <-> a e. (\ y, N[y / x] v) '' {x | p}
7 1, 6 ax_mp 
(a e. (\ y, N[y / x] v) '' {x | p} <-> E. x (p /\ a = v)) -> (a e. (\ x, v) '' {x | p} <-> E. x (p /\ a = v))
8 bitr4 
(a e. (\ y, N[y / x] v) '' {x | p} <-> E. y (y e. {x | p} /\ a = N[y / x] v)) ->
  (E. x (p /\ a = v) <-> E. y (y e. {x | p} /\ a = N[y / x] v)) ->
  (a e. (\ y, N[y / x] v) '' {x | p} <-> E. x (p /\ a = v))
9 ellamima 
a e. (\ y, N[y / x] v) '' {x | p} <-> E. y (y e. {x | p} /\ a = N[y / x] v)
10 8, 9 ax_mp 
(E. x (p /\ a = v) <-> E. y (y e. {x | p} /\ a = N[y / x] v)) -> (a e. (\ y, N[y / x] v) '' {x | p} <-> E. x (p /\ a = v))
11 nfv 
F/ y p /\ a = v
12 nfab1 
FS/ x {x | p}
13 12 nfel2 
F/ x y e. {x | p}
14 nfsbn1 
FN/ x N[y / x] v
15 14 nfeq2 
F/ x a = N[y / x] v
16 13, 15 nfan 
F/ x y e. {x | p} /\ a = N[y / x] v
17 elab 
y e. {x | p} <-> [y / x] p
18 sbq 
x = y -> (p <-> [y / x] p)
19 17, 18 syl6bbr 
x = y -> (p <-> y e. {x | p})
20 sbnq 
x = y -> v = N[y / x] v
21 20 eqeq2d 
x = y -> (a = v <-> a = N[y / x] v)
22 19, 21 aneqd 
x = y -> (p /\ a = v <-> y e. {x | p} /\ a = N[y / x] v)
23 11, 16, 22 cbvexh 
E. x (p /\ a = v) <-> E. y (y e. {x | p} /\ a = N[y / x] v)
24 10, 23 ax_mp 
a e. (\ y, N[y / x] v) '' {x | p} <-> E. x (p /\ a = v)
25 7, 24 ax_mp 
a e. (\ x, v) '' {x | p} <-> E. x (p /\ a = v)

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), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)