Theorem disj3 4429

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 557	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
2		eldif 3936	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	2	bibi2i 337	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
4	1, 3	bitr4i 278	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)))
5	4	albii 1819	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)))
6		disj1 4427	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
7		dfcleq 2728	. 2 ⊢ (𝐴 = (𝐴 ∖ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)))
8	5, 6, 7	3bitr4i 303	1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2108   ∖ cdif 3923   ∩ cin 3925  ∅c0 4308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-v 3461  df-dif 3929  df-in 3933  df-nul 4309

This theorem is referenced by:  disjel  4432  disj4  4434  uneqdifeq  4468  difprsn1  4776  diftpsn3  4778  ssunsn2  4803  orddif  6449  php  9219  phpOLD  9229  hartogslem1  9554  infeq5i  9648  cantnfp1lem3  9692  dju1dif  10185  infdju1  10202  ssxr  11302  dprd2da  20023  dmdprdsplit2lem  20026  ablfac1eulem  20053  lbsextlem4  21120  opsrtoslem2  22012  alexsublem  23980  volun  25496  lhop1lem  25968  ex-dif  30350  difeq  32445  imadifxp  32528  disjdsct  32626  fzodif1  32715  carsgclctunlem1  34295  probun  34397  ballotlemfp1  34470  bj-disj2r  36992  topdifinfeq  37314  finixpnum  37575  lindsadd  37583  poimirlem11  37601  poimirlem12  37602  poimirlem13  37603  poimirlem14  37604  poimirlem16  37606  poimirlem18  37608  poimirlem21  37611  poimirlem22  37612  poimirlem27  37617  asindmre  37673  kelac2  43036  pwfi2f1o  43067  iccdifioo  45492  iccdifprioo  45493