Step | Hyp | Ref | Expression |
1 |
|
bitr |
(a e. (\ x, v) '' A <-> E. y (y e. A /\ y, a e. \ x, v)) ->
(E. y (y e. A /\ y, a e. \ x, v) <-> E. x (x e. A /\ a = v)) ->
(a e. (\ x, v) '' A <-> E. x (x e. A /\ a = v)) |
2 |
|
elima |
a e. (\ x, v) '' A <-> E. y (y e. A /\ y, a e. \ x, v) |
3 |
1, 2 |
ax_mp |
(E. y (y e. A /\ y, a e. \ x, v) <-> E. x (x e. A /\ a = v)) -> (a e. (\ x, v) '' A <-> E. x (x e. A /\ a = v)) |
4 |
|
bitr4 |
(E. y (y e. A /\ y, a e. \ x, v) <-> E. y (y e. A /\ E. x (y = x /\ a = v))) ->
(E. x (x e. A /\ a = v) <-> E. y (y e. A /\ E. x (y = x /\ a = v))) ->
(E. y (y e. A /\ y, a e. \ x, v) <-> E. x (x e. A /\ a = v)) |
5 |
|
bitr |
(y, a e. \ x, v <-> E. x y, a = x, v) -> (E. x y, a = x, v <-> E. x (y = x /\ a = v)) -> (y, a e. \ x, v <-> E. x (y = x /\ a = v)) |
6 |
|
ellam |
y, a e. \ x, v <-> E. x y, a = x, v |
7 |
5, 6 |
ax_mp |
(E. x y, a = x, v <-> E. x (y = x /\ a = v)) -> (y, a e. \ x, v <-> E. x (y = x /\ a = v)) |
8 |
|
prth |
y, a = x, v <-> y = x /\ a = v |
9 |
8 |
exeqi |
E. x y, a = x, v <-> E. x (y = x /\ a = v) |
10 |
7, 9 |
ax_mp |
y, a e. \ x, v <-> E. x (y = x /\ a = v) |
11 |
10 |
rexeqi |
E. y (y e. A /\ y, a e. \ x, v) <-> E. y (y e. A /\ E. x (y = x /\ a = v)) |
12 |
4, 11 |
ax_mp |
(E. x (x e. A /\ a = v) <-> E. y (y e. A /\ E. x (y = x /\ a = v))) -> (E. y (y e. A /\ y, a e. \ x, v) <-> E. x (x e. A /\ a = v)) |
13 |
|
bitr3 |
(E. y (y = x /\ (y e. A /\ a = v)) <-> x e. A /\ a = v) ->
(E. y (y = x /\ (y e. A /\ a = v)) <-> E. y (y e. A /\ (y = x /\ a = v))) ->
(x e. A /\ a = v <-> E. y (y e. A /\ (y = x /\ a = v))) |
14 |
|
eleq1 |
y = x -> (y e. A <-> x e. A) |
15 |
14 |
aneq1d |
y = x -> (y e. A /\ a = v <-> x e. A /\ a = v) |
16 |
15 |
exeqe |
E. y (y = x /\ (y e. A /\ a = v)) <-> x e. A /\ a = v |
17 |
13, 16 |
ax_mp |
(E. y (y = x /\ (y e. A /\ a = v)) <-> E. y (y e. A /\ (y = x /\ a = v))) -> (x e. A /\ a = v <-> E. y (y e. A /\ (y = x /\ a = v))) |
18 |
|
anlass |
y = x /\ (y e. A /\ a = v) <-> y e. A /\ (y = x /\ a = v) |
19 |
18 |
exeqi |
E. y (y = x /\ (y e. A /\ a = v)) <-> E. y (y e. A /\ (y = x /\ a = v)) |
20 |
17, 19 |
ax_mp |
x e. A /\ a = v <-> E. y (y e. A /\ (y = x /\ a = v)) |
21 |
20 |
birexexi |
E. x (x e. A /\ a = v) <-> E. y (y e. A /\ E. x (y = x /\ a = v)) |
22 |
12, 21 |
ax_mp |
E. y (y e. A /\ y, a e. \ x, v) <-> E. x (x e. A /\ a = v) |
23 |
3, 22 |
ax_mp |
a e. (\ x, v) '' A <-> E. x (x e. A /\ a = v) |