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	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 )