Theorem disj3 4410

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 4052	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	2	bibi2i 340	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
4	1, 3	bitr4i 281	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)))
5	4	albii 1852	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)))
6		disj1 4408	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
7		dfcleq 2756	. 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 2147   ∖ cdif 4048   ∩ cin 4092  ∅c0 4281

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-v 3456  df-dif 4050  df-in 4094  df-nul 4282

This theorem is used by:  disjel  4413  disj4  4415  uneqdifeq  4451  difprsn1  4765  diftpsn3  4767  ssunsn2  4788  orddif  6487  php  9260  hartogslem1  9573  infeq5i  9674  cantnfp1lem3  9718  dju1dif  10290  infdju1  10307  ssxr  11418  dprd2da  20309  dmdprdsplit2lem  20312  ablfac1eulem  20339  lbsextlem4  21490  opsrtoslem2  22420  alexsublem  24418  volun  25921  lhop1lem  26388  ex-dif  31081  difeq  33213  imadifxp  33293  disjdsct  33393  fzodif1  33480  carsgclctunlem1  35060  probun  35162  ballotlemfp1  35235  bj-disj2r  38156  topdifinfeq  38541  finixpnum  38796  lindsadd  38804  poimirlem11  38817  poimirlem12  38818  poimirlem13  38819  poimirlem14  38820  poimirlem16  38822  poimirlem18  38824  poimirlem21  38827  poimirlem22  38828  poimirlem27  38833  asindmre  38889  kelac2  44333  pwfi2f1o  44364  iccdifioo  46800  iccdifprioo  46801