Step |
Hyp |
Ref |
Expression |
1 |
|
ax6ev |
|- E. x x = u |
2 |
|
hbae |
|- ( A. x x = y -> A. x A. x x = y ) |
3 |
|
ax7 |
|- ( x = y -> ( x = u -> y = u ) ) |
4 |
3
|
sps |
|- ( A. x x = y -> ( x = u -> y = u ) ) |
5 |
4
|
ancld |
|- ( A. x x = y -> ( x = u -> ( x = u /\ y = u ) ) ) |
6 |
2 5
|
eximdh |
|- ( A. x x = y -> ( E. x x = u -> E. x ( x = u /\ y = u ) ) ) |
7 |
1 6
|
mpi |
|- ( A. x x = y -> E. x ( x = u /\ y = u ) ) |
8 |
7
|
axc4i |
|- ( A. x x = y -> A. x E. x ( x = u /\ y = u ) ) |
9 |
|
axc11 |
|- ( A. x x = y -> ( A. x E. x ( x = u /\ y = u ) -> A. y E. x ( x = u /\ y = u ) ) ) |
10 |
8 9
|
mpd |
|- ( A. x x = y -> A. y E. x ( x = u /\ y = u ) ) |
11 |
|
19.2 |
|- ( A. y E. x ( x = u /\ y = u ) -> E. y E. x ( x = u /\ y = u ) ) |
12 |
10 11
|
syl |
|- ( A. x x = y -> E. y E. x ( x = u /\ y = u ) ) |
13 |
|
excomim |
|- ( E. y E. x ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = u ) ) |
14 |
12 13
|
syl |
|- ( A. x x = y -> E. x E. y ( x = u /\ y = u ) ) |
15 |
|
equtrr |
|- ( u = v -> ( y = u -> y = v ) ) |
16 |
15
|
anim2d |
|- ( u = v -> ( ( x = u /\ y = u ) -> ( x = u /\ y = v ) ) ) |
17 |
16
|
2eximdv |
|- ( u = v -> ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) ) |
18 |
14 17
|
syl5com |
|- ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) |