This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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