MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reldisj Structured version   Visualization version   GIF version

Theorem reldisj 4450
Description: Two ways of saying that two classes are disjoint, using the complement of 𝐵 relative to a universe 𝐶. (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid ax-12 2169. (Revised by Gino Giotto, 28-Jun-2024.)
Assertion
Ref Expression
reldisj (𝐴𝐶 → ((𝐴𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶𝐵)))

Proof of Theorem reldisj
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfss2 3967 . . . 4 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
2 eleq1w 2814 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
3 eleq1w 2814 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝐶𝑦𝐶))
42, 3imbi12d 343 . . . . . 6 (𝑥 = 𝑦 → ((𝑥𝐴𝑥𝐶) ↔ (𝑦𝐴𝑦𝐶)))
54spw 2035 . . . . 5 (∀𝑥(𝑥𝐴𝑥𝐶) → (𝑥𝐴𝑥𝐶))
6 pm5.44 541 . . . . . 6 ((𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴 → (𝑥𝐶 ∧ ¬ 𝑥𝐵))))
7 eldif 3957 . . . . . . 7 (𝑥 ∈ (𝐶𝐵) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐵))
87imbi2i 335 . . . . . 6 ((𝑥𝐴𝑥 ∈ (𝐶𝐵)) ↔ (𝑥𝐴 → (𝑥𝐶 ∧ ¬ 𝑥𝐵)))
96, 8bitr4di 288 . . . . 5 ((𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
105, 9syl 17 . . . 4 (∀𝑥(𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
111, 10sylbi 216 . . 3 (𝐴𝐶 → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
1211albidv 1921 . 2 (𝐴𝐶 → (∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐶𝐵))))
13 disj1 4449 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
14 dfss2 3967 . 2 (𝐴 ⊆ (𝐶𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐶𝐵)))
1512, 13, 143bitr4g 313 1 (𝐴𝐶 → ((𝐴𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wal 1537   = wceq 1539  wcel 2104  cdif 3944  cin 3946  wss 3947  c0 4321
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-v 3474  df-dif 3950  df-in 3954  df-ss 3964  df-nul 4322
This theorem is referenced by:  disj2  4456  ssdifsn  4790  oacomf1olem  8566  domdifsn  9056  elfiun  9427  cantnfp1lem3  9677  ssxr  11287  structcnvcnv  17090  fidomndrng  21126  elcls  22797  ist1-2  23071  nrmsep2  23080  nrmsep  23081  isnrm3  23083  isreg2  23101  hauscmplem  23130  connsub  23145  iunconnlem  23151  llycmpkgen2  23274  hausdiag  23369  trfil3  23612  isufil2  23632  filufint  23644  blcld  24234  i1fima2  25428  i1fd  25430  nbgrssvwo2  28886  pliguhgr  30006  symgcom2  32515  inunissunidif  36559  poimirlem15  36806  itg2addnclem2  36843  ntrk0kbimka  43092  ntrneicls11  43143  gneispace  43187  opndisj  47622  seposep  47645
  Copyright terms: Public domain W3C validator