Step | Hyp | Ref | Expression |
1 |
|
bitr |
(a1 e. Ran (sn (x, y)) <-> E. a2 a2, a1 e. sn (x, y)) -> (E. a2 a2, a1 e. sn (x, y) <-> a1 e. sn y) -> (a1 e. Ran (sn (x, y)) <-> a1 e. sn y) |
2 |
|
elrn |
a1 e. Ran (sn (x, y)) <-> E. a2 a2, a1 e. sn (x, y) |
3 |
1, 2 |
ax_mp |
(E. a2 a2, a1 e. sn (x, y) <-> a1 e. sn y) -> (a1 e. Ran (sn (x, y)) <-> a1 e. sn y) |
4 |
|
bitr4 |
(E. a2 a2, a1 e. sn (x, y) <-> E. a2 (a2 = x /\ a1 = y)) -> (a1 e. sn y <-> E. a2 (a2 = x /\ a1 = y)) -> (E. a2 a2, a1 e. sn (x, y) <-> a1 e. sn y) |
5 |
|
bitr |
(a2, a1 e. sn (x, y) <-> a2, a1 = x, y) -> (a2, a1 = x, y <-> a2 = x /\ a1 = y) -> (a2, a1 e. sn (x, y) <-> a2 = x /\ a1 = y) |
6 |
|
elsn |
a2, a1 e. sn (x, y) <-> a2, a1 = x, y |
7 |
5, 6 |
ax_mp |
(a2, a1 = x, y <-> a2 = x /\ a1 = y) -> (a2, a1 e. sn (x, y) <-> a2 = x /\ a1 = y) |
8 |
|
prth |
a2, a1 = x, y <-> a2 = x /\ a1 = y |
9 |
7, 8 |
ax_mp |
a2, a1 e. sn (x, y) <-> a2 = x /\ a1 = y |
10 |
9 |
exeqi |
E. a2 a2, a1 e. sn (x, y) <-> E. a2 (a2 = x /\ a1 = y) |
11 |
4, 10 |
ax_mp |
(a1 e. sn y <-> E. a2 (a2 = x /\ a1 = y)) -> (E. a2 a2, a1 e. sn (x, y) <-> a1 e. sn y) |
12 |
|
bitr4 |
(a1 e. sn y <-> a1 = y) -> (E. a2 (a2 = x /\ a1 = y) <-> a1 = y) -> (a1 e. sn y <-> E. a2 (a2 = x /\ a1 = y)) |
13 |
|
elsn |
a1 e. sn y <-> a1 = y |
14 |
12, 13 |
ax_mp |
(E. a2 (a2 = x /\ a1 = y) <-> a1 = y) -> (a1 e. sn y <-> E. a2 (a2 = x /\ a1 = y)) |
15 |
|
biidd |
a2 = x -> (a1 = y <-> a1 = y) |
16 |
15 |
exeqe |
E. a2 (a2 = x /\ a1 = y) <-> a1 = y |
17 |
14, 16 |
ax_mp |
a1 e. sn y <-> E. a2 (a2 = x /\ a1 = y) |
18 |
11, 17 |
ax_mp |
E. a2 a2, a1 e. sn (x, y) <-> a1 e. sn y |
19 |
3, 18 |
ax_mp |
a1 e. Ran (sn (x, y)) <-> a1 e. sn y |
20 |
19 |
ax_gen |
A. a1 (a1 e. Ran (sn (x, y)) <-> a1 e. sn y) |
21 |
20 |
conv eqs |
Ran (sn (x, y)) == sn y |