Step |
Hyp |
Ref |
Expression |
1 |
|
2eu1 |
|- ( A. x E* y ph -> ( E! x E! y ph <-> ( E! x E. y ph /\ E! y E. x ph ) ) ) |
2 |
1
|
pm5.32ri |
|- ( ( E! x E! y ph /\ A. x E* y ph ) <-> ( ( E! x E. y ph /\ E! y E. x ph ) /\ A. x E* y ph ) ) |
3 |
|
eumo |
|- ( E! y E. x ph -> E* y E. x ph ) |
4 |
3
|
adantl |
|- ( ( E! x E. y ph /\ E! y E. x ph ) -> E* y E. x ph ) |
5 |
|
2moex |
|- ( E* y E. x ph -> A. x E* y ph ) |
6 |
4 5
|
syl |
|- ( ( E! x E. y ph /\ E! y E. x ph ) -> A. x E* y ph ) |
7 |
6
|
pm4.71i |
|- ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( ( E! x E. y ph /\ E! y E. x ph ) /\ A. x E* y ph ) ) |
8 |
|
2eu4 |
|- ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) ) |
9 |
2 7 8
|
3bitr2i |
|- ( ( E! x E! y ph /\ A. x E* y ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) ) |