Theorem disj3 4459

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1534   = wceq 1536   ∈ wcel 2105   ∖ cdif 3959   ∩ cin 3961  ∅c0 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-v 3479  df-dif 3965  df-in 3969  df-nul 4339

This theorem is referenced by:  disjel  4462  disj4  4464  uneqdifeq  4498  difprsn1  4804  diftpsn3  4806  ssunsn2  4831  orddif  6481  php  9244  phpOLD  9256  hartogslem1  9579  infeq5i  9673  cantnfp1lem3  9717  dju1dif  10210  infdju1  10227  ssxr  11327  dprd2da  20076  dmdprdsplit2lem  20079  ablfac1eulem  20106  lbsextlem4  21180  opsrtoslem2  22097  alexsublem  24067  volun  25593  lhop1lem  26066  ex-dif  30451  difeq  32545  imadifxp  32620  disjdsct  32717  fzodif1  32800  carsgclctunlem1  34298  probun  34400  ballotlemfp1  34472  bj-disj2r  37010  topdifinfeq  37332  finixpnum  37591  lindsadd  37599  poimirlem11  37617  poimirlem12  37618  poimirlem13  37619  poimirlem14  37620  poimirlem16  37622  poimirlem18  37624  poimirlem21  37627  poimirlem22  37628  poimirlem27  37633  asindmre  37689  kelac2  43053  pwfi2f1o  43084  iccdifioo  45467  iccdifprioo  45468