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