Theorem disj 4385

Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) Avoid ax-10 2152, ax-11 2168, ax-12 2189. (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 3897	. . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
2	1	eqeq1i 2745	. . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = ∅)
3		eleq1w 2823	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
4		eleq1w 2823	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
5	3, 4	anbi12d 638	. . . 4 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
6	5	eqabcbw 2814	. . 3 ⊢ ({𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} = ∅ ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅))
7		imnan 400	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
8		noel 4273	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
9	8	nbn 373	. . . . 5 ⊢ (¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅))
10	7, 9	bitr2i 277	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
11	10	albii 1826	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
12	2, 6, 11	3bitri 298	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
13		df-ral 3055	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
14	12, 13	bitr4i 279	1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1545   = wceq 1547   ∈ wcel 2119  {cab 2718  ∀wral 3054   ∩ cin 3889  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-dif 3893  df-in 3897  df-nul 4269

This theorem is referenced by:  disjr  4386  disj1  4387  disjne  4390  disjord  5068  disjiund  5070  otiunsndisj  5468  dfpo2  6254  onxpdisj  6444  f0rn0  6719  onint  7740  zfreg  9508  kmlem4  10074  fin23lem30  10262  fin23lem31  10263  isf32lem3  10275  fpwwe2  10564  renfdisj  11203  fvinim0ffz  13742  s3iunsndisj  14928  metdsge  24840  sltsdisj  27820  dfpth2  29822  2wspmdisj  30432  subfacp1lem1  35414  disjabso  45426  dvmptfprodlem  46394  stoweidlem26  46476  stoweidlem59  46509  iundjiunlem  46909  otiunsndisjX  47749  upgrimpths  48407