Theorem disjex

Description: Two ways to say that two classes are disjoint (or equal). (Contributed by Thierry Arnoux, 4-Oct-2016)

	Ref	Expression
Assertion	disjex	|- ( ( E. z ( z e. A /\ z e. B ) -> A = B ) <-> ( A = B \/ ( A i^i B ) = (/) ) )

Proof

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 ) = (/) ) )