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

Theorem reldisj 4316
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.)
Assertion
Ref Expression
reldisj (𝐴𝐶 → ((𝐴𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶𝐵)))

Proof of Theorem reldisj
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dfss2 3877 . . . 4 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
2 pm5.44 543 . . . . . 6 ((𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴 → (𝑥𝐶 ∧ ¬ 𝑥𝐵))))
3 eldif 3869 . . . . . . 7 (𝑥 ∈ (𝐶𝐵) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐵))
43imbi2i 337 . . . . . 6 ((𝑥𝐴𝑥 ∈ (𝐶𝐵)) ↔ (𝑥𝐴 → (𝑥𝐶 ∧ ¬ 𝑥𝐵)))
52, 4syl6bbr 290 . . . . 5 ((𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
65sps 2148 . . . 4 (∀𝑥(𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
71, 6sylbi 218 . . 3 (𝐴𝐶 → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
87albidv 1898 . 2 (𝐴𝐶 → (∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐶𝐵))))
9 disj1 4315 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
10 dfss2 3877 . 2 (𝐴 ⊆ (𝐶𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐶𝐵)))
118, 9, 103bitr4g 315 1 (𝐴𝐶 → ((𝐴𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wal 1520   = wceq 1522  wcel 2081  cdif 3856  cin 3858  wss 3859  c0 4211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-v 3439  df-dif 3862  df-in 3866  df-ss 3874  df-nul 4212
This theorem is referenced by:  disj2  4321  ssdifsn  4627  oacomf1olem  8040  domdifsn  8447  elfiun  8740  cantnfp1lem3  8989  ssxr  10557  structcnvcnv  16326  fidomndrng  19769  elcls  21365  ist1-2  21639  nrmsep2  21648  nrmsep  21649  isnrm3  21651  isreg2  21669  hauscmplem  21698  connsub  21713  iunconnlem  21719  llycmpkgen2  21842  hausdiag  21937  trfil3  22180  isufil2  22200  filufint  22212  blcld  22798  i1fima2  23963  i1fd  23965  nbgrssvwo2  26827  pliguhgr  27954  symgcom2  30387  inunissunidif  34187  poimirlem15  34438  itg2addnclem2  34475  ntrk0kbimka  39874  ntrneicls11  39925  gneispace  39969
  Copyright terms: Public domain W3C validator