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

Metamath Proof Explorer

Theorem disj

Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004) Avoid ax-10 , ax-11 , ax-12 . (Revised by GG, 28-Jun-2024)

Ref Expression
Assertion disj ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 df-in ⊢ ( 𝐴 ∩ 𝐵 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) }
2 1 eqeq1i ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } = ∅ )
3 eleq1w ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
4 eleq1w ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
5 3 4 anbi12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
6 5 eqabcbw ⊢ ( { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } = ∅ ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ∅ ) )
7 imnan ⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
8 noel ⊢ ¬ 𝑥 ∈ ∅
9 8 nbn ⊢ ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ∅ ) )
10 7 9 bitr2i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ∅ ) ↔ ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
11 10 albii ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ∅ ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
12 2 6 11 3bitri ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
13 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
14 12 13 bitr4i ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 )