Theorem elrlam ≪ | index | src | ≫ 

theorem elrlam (p: nat) {x: nat} (a: nat) (b: nat x):
  $ p e. \. x e. a, b <-> E. x (x e. a /\ p = x, b) $;
StepHypRefExpression
1 bitr 
(p e. \. x e. a, b <-> p e. (\ x, b) |` a) -> (p e. (\ x, b) |` a <-> E. x (x e. a /\ p = x, b)) -> (p e. \. x e. a, b <-> E. x (x e. a /\ p = x, b))
2 ellower 
finite ((\ x, b) |` a) -> (p e. lower ((\ x, b) |` a) <-> p e. (\ x, b) |` a)
3 2 conv rlam 
finite ((\ x, b) |` a) -> (p e. \. x e. a, b <-> p e. (\ x, b) |` a)
4 finlam 
finite a -> finite ((\ x, b) |` a)
5 finns 
finite a
6 4, 5 ax_mp 
finite ((\ x, b) |` a)
7 3, 6 ax_mp 
p e. \. x e. a, b <-> p e. (\ x, b) |` a
8 1, 7 ax_mp 
(p e. (\ x, b) |` a <-> E. x (x e. a /\ p = x, b)) -> (p e. \. x e. a, b <-> E. x (x e. a /\ p = x, b))
9 bitr 
(p e. (\ x, b) |` a <-> p e. \ x, b /\ fst p e. a) ->
  (p e. \ x, b /\ fst p e. a <-> E. x (x e. a /\ p = x, b)) ->
  (p e. (\ x, b) |` a <-> E. x (x e. a /\ p = x, b))
10 elres 
p e. (\ x, b) |` a <-> p e. \ x, b /\ fst p e. a
11 9, 10 ax_mp 
(p e. \ x, b /\ fst p e. a <-> E. x (x e. a /\ p = x, b)) -> (p e. (\ x, b) |` a <-> E. x (x e. a /\ p = x, b))
12 bitr 
(p e. \ x, b /\ fst p e. a <-> E. x p = x, b /\ fst p e. a) ->
  (E. x p = x, b /\ fst p e. a <-> E. x (x e. a /\ p = x, b)) ->
  (p e. \ x, b /\ fst p e. a <-> E. x (x e. a /\ p = x, b))
13 ellam 
p e. \ x, b <-> E. x p = x, b
14 13 aneq1i 
p e. \ x, b /\ fst p e. a <-> E. x p = x, b /\ fst p e. a
15 12, 14 ax_mp 
(E. x p = x, b /\ fst p e. a <-> E. x (x e. a /\ p = x, b)) -> (p e. \ x, b /\ fst p e. a <-> E. x (x e. a /\ p = x, b))
16 bitr3 
(E. x (p = x, b /\ fst p e. a) <-> E. x p = x, b /\ fst p e. a) ->
  (E. x (p = x, b /\ fst p e. a) <-> E. x (x e. a /\ p = x, b)) ->
  (E. x p = x, b /\ fst p e. a <-> E. x (x e. a /\ p = x, b))
17 exan2 
E. x (p = x, b /\ fst p e. a) <-> E. x p = x, b /\ fst p e. a
18 16, 17 ax_mp 
(E. x (p = x, b /\ fst p e. a) <-> E. x (x e. a /\ p = x, b)) -> (E. x p = x, b /\ fst p e. a <-> E. x (x e. a /\ p = x, b))
19 bitr 
(p = x, b /\ fst p e. a <-> fst p e. a /\ p = x, b) -> (fst p e. a /\ p = x, b <-> x e. a /\ p = x, b) -> (p = x, b /\ fst p e. a <-> x e. a /\ p = x, b)
20 ancomb 
p = x, b /\ fst p e. a <-> fst p e. a /\ p = x, b
21 19, 20 ax_mp 
(fst p e. a /\ p = x, b <-> x e. a /\ p = x, b) -> (p = x, b /\ fst p e. a <-> x e. a /\ p = x, b)
22 aneq1a 
(p = x, b -> (fst p e. a <-> x e. a)) -> (fst p e. a /\ p = x, b <-> x e. a /\ p = x, b)
23 fstpr 
fst (x, b) = x
24 fsteq 
p = x, b -> fst p = fst (x, b)
25 23, 24 syl6eq 
p = x, b -> fst p = x
26 25 eleq1d 
p = x, b -> (fst p e. a <-> x e. a)
27 22, 26 ax_mp 
fst p e. a /\ p = x, b <-> x e. a /\ p = x, b
28 21, 27 ax_mp 
p = x, b /\ fst p e. a <-> x e. a /\ p = x, b
29 28 exeqi 
E. x (p = x, b /\ fst p e. a) <-> E. x (x e. a /\ p = x, b)
30 18, 29 ax_mp 
E. x p = x, b /\ fst p e. a <-> E. x (x e. a /\ p = x, b)
31 15, 30 ax_mp 
p e. \ x, b /\ fst p e. a <-> E. x (x e. a /\ p = x, b)
32 11, 31 ax_mp 
p e. (\ x, b) |` a <-> E. x (x e. a /\ p = x, b)
33 8, 32 ax_mp 
p e. \. x e. a, b <-> E. x (x e. a /\ p = 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), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)