Theorem disj3 4407

Description: Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.)

Assertion

Ref	Expression
disj3	⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵))

Proof of Theorem disj3

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pm4.71 567	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
2		eldif 3909	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	2	bibi2i 340	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
4	1, 3	bitr4i 281	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)))
5	4	albii 1852	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)))
6		disj1 4405	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
7		dfcleq 2754	. 2 ⊢ (𝐴 = (𝐴 ∖ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)))
8	5, 6, 7	3bitr4i 306	1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570   ∈ wcel 2145   ∖ cdif 3896   ∩ 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-v 3453  df-dif 3902  df-in 3906  df-nul 4280

This theorem is used by:  disjel  4410  disj4  4412  uneqdifeq  4448  difprsn1  4763  diftpsn3  4765  ssunsn2  4788  orddif  6460  php  9215  hartogslem1  9529  infeq5i  9630  cantnfp1lem3  9674  dju1dif  10244  infdju1  10261  ssxr  11372  dprd2da  20251  dmdprdsplit2lem  20254  ablfac1eulem  20281  lbsextlem4  21432  opsrtoslem2  22358  alexsublem  24356  volun  25859  lhop1lem  26326  ex-dif  31017  difeq  33107  imadifxp  33188  disjdsct  33289  fzodif1  33377  carsgclctunlem1  34942  probun  35044  ballotlemfp1  35117  bj-disj2r  37921  topdifinfeq  38253  finixpnum  38508  lindsadd  38516  poimirlem11  38529  poimirlem12  38530  poimirlem13  38531  poimirlem14  38532  poimirlem16  38534  poimirlem18  38536  poimirlem21  38539  poimirlem22  38540  poimirlem27  38545  asindmre  38601  kelac2  44051  pwfi2f1o  44082  iccdifioo  46496  iccdifprioo  46497