Theorem disj3 4393

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 558	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
2		eldif 3902	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	2	bibi2i 338	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
4	1, 3	bitr4i 277	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)))
5	4	albii 1826	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)))
6		disj1 4390	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
7		dfcleq 2733	. 2 ⊢ (𝐴 = (𝐴 ∖ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)))
8	5, 6, 7	3bitr4i 303	1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1540   = wceq 1542   ∈ wcel 2110   ∖ cdif 3889   ∩ cin 3891  ∅c0 4262

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ral 3071  df-v 3433  df-dif 3895  df-in 3899  df-nul 4263

This theorem is referenced by:  disjel  4396  disj4  4398  uneqdifeq  4429  difprsn1  4739  diftpsn3  4741  ssunsn2  4766  orddif  6358  php  8983  phpOLD  8995  hartogslem1  9289  infeq5i  9382  cantnfp1lem3  9426  dju1dif  9939  infdju1  9956  ssxr  11055  dprd2da  19656  dmdprdsplit2lem  19659  ablfac1eulem  19686  lbsextlem4  20434  opsrtoslem2  21274  alexsublem  23206  volun  24720  lhop1lem  25188  ex-dif  28796  difeq  30874  imadifxp  30949  disjdsct  31044  fzodif1  31123  carsgclctunlem1  32293  probun  32395  ballotlemfp1  32467  bj-disj2r  35227  topdifinfeq  35530  finixpnum  35771  lindsadd  35779  poimirlem11  35797  poimirlem12  35798  poimirlem13  35799  poimirlem14  35800  poimirlem16  35802  poimirlem18  35804  poimirlem21  35807  poimirlem22  35808  poimirlem27  35813  asindmre  35869  kelac2  40899  pwfi2f1o  40930  iccdifioo  43035  iccdifprioo  43036