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	⊢ ( ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝐴 = 𝐵 ) ↔ ( 𝐴 = 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		orcom	⊢ ( ( 𝐴 = 𝐵 ∨ ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ↔ ( ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ∨ 𝐴 = 𝐵 ) )
2		df-in	⊢ ( 𝐴 ∩ 𝐵 ) = { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) }
3	2	neeq1i	⊢ ( ( 𝐴 ∩ 𝐵 ) ≠ ∅ ↔ { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } ≠ ∅ )
4		abn0	⊢ ( { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } ≠ ∅ ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
5	3 4	bitr2i	⊢ ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ↔ ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
6	5	necon2bbii	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
7	6	orbi2i	⊢ ( ( 𝐴 = 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) ↔ ( 𝐴 = 𝐵 ∨ ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) )
8		imor	⊢ ( ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝐴 = 𝐵 ) ↔ ( ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ∨ 𝐴 = 𝐵 ) )
9	1 7 8	3bitr4ri	⊢ ( ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝐴 = 𝐵 ) ↔ ( 𝐴 = 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) )