Step |
Hyp |
Ref |
Expression |
1 |
|
19.21v |
|- ( A. y ( x e. A -> ( y e. A -> x = y ) ) <-> ( x e. A -> A. y ( y e. A -> x = y ) ) ) |
2 |
|
impexp |
|- ( ( ( x e. A /\ y e. A ) -> x = y ) <-> ( x e. A -> ( y e. A -> x = y ) ) ) |
3 |
2
|
albii |
|- ( A. y ( ( x e. A /\ y e. A ) -> x = y ) <-> A. y ( x e. A -> ( y e. A -> x = y ) ) ) |
4 |
|
df-ral |
|- ( A. y e. A x = y <-> A. y ( y e. A -> x = y ) ) |
5 |
4
|
imbi2i |
|- ( ( x e. A -> A. y e. A x = y ) <-> ( x e. A -> A. y ( y e. A -> x = y ) ) ) |
6 |
1 3 5
|
3bitr4i |
|- ( A. y ( ( x e. A /\ y e. A ) -> x = y ) <-> ( x e. A -> A. y e. A x = y ) ) |
7 |
6
|
albii |
|- ( A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) <-> A. x ( x e. A -> A. y e. A x = y ) ) |
8 |
|
eleq1w |
|- ( x = y -> ( x e. A <-> y e. A ) ) |
9 |
8
|
mo4 |
|- ( E* x x e. A <-> A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) ) |
10 |
|
df-ral |
|- ( A. x e. A A. y e. A x = y <-> A. x ( x e. A -> A. y e. A x = y ) ) |
11 |
7 9 10
|
3bitr4i |
|- ( E* x x e. A <-> A. x e. A A. y e. A x = y ) |