Theorem disj3 4414

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 3916	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	2	bibi2i 340	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
4	1, 3	bitr4i 281	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)))
5	4	albii 1852	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)))
6		disj1 4412	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
7		dfcleq 2758	. 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 2146   ∖ cdif 3903   ∩ cin 3905  ∅c0 4286

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-v 3459  df-dif 3909  df-in 3913  df-nul 4287

This theorem is used by:  disjel  4417  disj4  4419  uneqdifeq  4455  difprsn1  4770  diftpsn3  4772  ssunsn2  4795  orddif  6463  php  9198  hartogslem1  9511  infeq5i  9612  cantnfp1lem3  9656  dju1dif  10172  infdju1  10189  ssxr  11294  dprd2da  20158  dmdprdsplit2lem  20161  ablfac1eulem  20188  lbsextlem4  21335  opsrtoslem2  22257  alexsublem  24252  volun  25755  lhop1lem  26223  ex-dif  30845  difeq  32935  imadifxp  33017  disjdsct  33119  fzodif1  33207  carsgclctunlem1  34772  probun  34874  ballotlemfp1  34947  bj-disj2r  37721  topdifinfeq  38053  finixpnum  38313  lindsadd  38321  poimirlem11  38339  poimirlem12  38340  poimirlem13  38341  poimirlem14  38342  poimirlem16  38344  poimirlem18  38346  poimirlem21  38349  poimirlem22  38350  poimirlem27  38355  asindmre  38411  kelac2  43850  pwfi2f1o  43881  iccdifioo  46289  iccdifprioo  46290