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

Theorem reldisj 4181
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 3749 . . . 4 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
2 pm5.44 538 . . . . . 6 ((𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴 → (𝑥𝐶 ∧ ¬ 𝑥𝐵))))
3 eldif 3742 . . . . . . 7 (𝑥 ∈ (𝐶𝐵) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐵))
43imbi2i 327 . . . . . 6 ((𝑥𝐴𝑥 ∈ (𝐶𝐵)) ↔ (𝑥𝐴 → (𝑥𝐶 ∧ ¬ 𝑥𝐵)))
52, 4syl6bbr 280 . . . . 5 ((𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
65sps 2217 . . . 4 (∀𝑥(𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
71, 6sylbi 208 . . 3 (𝐴𝐶 → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
87albidv 2015 . 2 (𝐴𝐶 → (∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐶𝐵))))
9 disj1 4180 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
10 dfss2 3749 . 2 (𝐴 ⊆ (𝐶𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐶𝐵)))
118, 9, 103bitr4g 305 1 (𝐴𝐶 → ((𝐴𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wal 1650   = wceq 1652  wcel 2155  cdif 3729  cin 3731  wss 3732  c0 4079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-v 3352  df-dif 3735  df-in 3739  df-ss 3746  df-nul 4080
This theorem is referenced by:  disj2  4186  ssdifsn  4473  oacomf1olem  7849  domdifsn  8250  elfiun  8543  cantnfp1lem3  8792  ssxr  10361  structcnvcnv  16144  fidomndrng  19581  elcls  21157  ist1-2  21431  nrmsep2  21440  nrmsep  21441  isnrm3  21443  isreg2  21461  hauscmplem  21489  connsub  21504  iunconnlem  21510  llycmpkgen2  21633  hausdiag  21728  trfil3  21971  isufil2  21991  filufint  22003  blcld  22589  i1fima2  23737  i1fd  23739  nbgrssvwo2  26537  nbgrssvwo2OLD  26540  pliguhgr  27797  poimirlem15  33848  itg2addnclem2  33885  ntrk0kbimka  39011  ntrneicls11  39062  gneispace  39106
  Copyright terms: Public domain W3C validator