Theorem disj 4403

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

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem disj

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-in 3906	. . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
2	1	eqeq1i 2766	. . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = ∅)
3		eleq1w 2844	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
4		eleq1w 2844	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
5	3, 4	anbi12d 644	. . . 4 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
6	5	eqabcbw 2835	. . 3 ⊢ ({𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = ∅ ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅))
7		imnan 405	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
8		noel 4284	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
9	8	nbn 375	. . . . 5 ⊢ (¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅))
10	7, 9	bitr2i 279	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
11	10	albii 1852	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
12	2, 6, 11	3bitri 300	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
13		df-ral 3078	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
14	12, 13	bitr4i 281	1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570   ∈ wcel 2145  {cab 2739  ∀wral 3077   ∩ cin 3898  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-dif 3902  df-in 3906  df-nul 4280

This theorem is used by:  disjr  4404  disj1  4405  disjne  4408  disjord  5092  disjiund  5094  otiunsndisj  5493  dfpo2  6292  onxpdisj  6483  f0rn0  6759  onint  7793  zfreg  9574  kmlem4  10213  fin23lem30  10401  fin23lem31  10402  isf32lem3  10414  fpwwe2  10709  renfdisj  11350  fvinim0ffz  13904  s3iunsndisj  15101  metdsge  25149  sltsdisj  28171  dfpth2  30296  2wspmdisj  30920  subfacp1lem1  35913  disjabso  45917  dvmptfprodlem  46898  stoweidlem26  46980  stoweidlem59  47013  iundjiunlem  47413  otiunsndisjX  48293  upgrimpths  48951