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 Gino Giotto, 28-Jun-2024)

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

Proof

Step	Hyp	Ref	Expression
1		df-in	⊢ ( 𝐴 ∩ 𝐵 ) = { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) }
2	1	eqeq1i	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } = ∅ )
3		dfcleq	⊢ ( ∅ = { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } ↔ ∀ 𝑥 ( 𝑥 ∈ ∅ ↔ 𝑥 ∈ { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } ) )
4		df-clab	⊢ ( 𝑥 ∈ { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } ↔ [ 𝑥 / 𝑧 ] ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
5		sb6	⊢ ( [ 𝑥 / 𝑧 ] ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ↔ ∀ 𝑧 ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) )
6		id	⊢ ( 𝑧 = 𝑥 → 𝑧 = 𝑥 )
7		eleq1w	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
8	7	biimpd	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐴 → 𝑥 ∈ 𝐴 ) )
9		eleq1w	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
10	9	biimpd	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐵 → 𝑥 ∈ 𝐵 ) )
11	8 10	anim12d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
12	6 11	embantd	⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
13	12	spimvw	⊢ ( ∀ 𝑧 ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
14		eleq1a	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝑥 → 𝑧 ∈ 𝐴 ) )
15		eleq1a	⊢ ( 𝑥 ∈ 𝐵 → ( 𝑧 = 𝑥 → 𝑧 ∈ 𝐵 ) )
16	14 15	anim12ii	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) )
17	16	alrimiv	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑧 ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) )
18	13 17	impbii	⊢ ( ∀ 𝑧 ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
19	4 5 18	3bitri	⊢ ( 𝑥 ∈ { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
20	19	bibi2i	⊢ ( ( 𝑥 ∈ ∅ ↔ 𝑥 ∈ { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } ) ↔ ( 𝑥 ∈ ∅ ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
21	20	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ ∅ ↔ 𝑥 ∈ { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } ) ↔ ∀ 𝑥 ( 𝑥 ∈ ∅ ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
22	3 21	bitri	⊢ ( ∅ = { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } ↔ ∀ 𝑥 ( 𝑥 ∈ ∅ ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
23		eqcom	⊢ ( { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } = ∅ ↔ ∅ = { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } )
24		bicom	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ∅ ) ↔ ( 𝑥 ∈ ∅ ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
25	24	albii	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ∅ ) ↔ ∀ 𝑥 ( 𝑥 ∈ ∅ ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
26	22 23 25	3bitr4i	⊢ ( { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } = ∅ ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ∅ ) )
27		imnan	⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
28		noel	⊢ ¬ 𝑥 ∈ ∅
29	28	nbn	⊢ ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ∅ ) )
30	27 29	bitr2i	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ∅ ) ↔ ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
31	30	albii	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ ∅ ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
32	2 26 31	3bitri	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
33		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
34	32 33	bitr4i	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 )