Step |
Hyp |
Ref |
Expression |
1 |
|
orcom |
|- ( ( A = B \/ -. E. z ( z e. A /\ z e. B ) ) <-> ( -. E. z ( z e. A /\ z e. B ) \/ A = B ) ) |
2 |
|
df-in |
|- ( A i^i B ) = { z | ( z e. A /\ z e. B ) } |
3 |
2
|
neeq1i |
|- ( ( A i^i B ) =/= (/) <-> { z | ( z e. A /\ z e. B ) } =/= (/) ) |
4 |
|
abn0 |
|- ( { z | ( z e. A /\ z e. B ) } =/= (/) <-> E. z ( z e. A /\ z e. B ) ) |
5 |
3 4
|
bitr2i |
|- ( E. z ( z e. A /\ z e. B ) <-> ( A i^i B ) =/= (/) ) |
6 |
5
|
necon2bbii |
|- ( ( A i^i B ) = (/) <-> -. E. z ( z e. A /\ z e. B ) ) |
7 |
6
|
orbi2i |
|- ( ( A = B \/ ( A i^i B ) = (/) ) <-> ( A = B \/ -. E. z ( z e. A /\ z e. B ) ) ) |
8 |
|
imor |
|- ( ( E. z ( z e. A /\ z e. B ) -> A = B ) <-> ( -. E. z ( z e. A /\ z e. B ) \/ A = B ) ) |
9 |
1 7 8
|
3bitr4ri |
|- ( ( E. z ( z e. A /\ z e. B ) -> A = B ) <-> ( A = B \/ ( A i^i B ) = (/) ) ) |