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

Theorem reldisj 4449
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 2172. (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 3966 . . . 4 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
2 eleq1w 2817 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
3 eleq1w 2817 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝐶𝑦𝐶))
42, 3imbi12d 345 . . . . . 6 (𝑥 = 𝑦 → ((𝑥𝐴𝑥𝐶) ↔ (𝑦𝐴𝑦𝐶)))
54spw 2038 . . . . 5 (∀𝑥(𝑥𝐴𝑥𝐶) → (𝑥𝐴𝑥𝐶))
6 pm5.44 544 . . . . . 6 ((𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴 → (𝑥𝐶 ∧ ¬ 𝑥𝐵))))
7 eldif 3956 . . . . . . 7 (𝑥 ∈ (𝐶𝐵) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐵))
87imbi2i 336 . . . . . 6 ((𝑥𝐴𝑥 ∈ (𝐶𝐵)) ↔ (𝑥𝐴 → (𝑥𝐶 ∧ ¬ 𝑥𝐵)))
96, 8bitr4di 289 . . . . 5 ((𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
105, 9syl 17 . . . 4 (∀𝑥(𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
111, 10sylbi 216 . . 3 (𝐴𝐶 → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
1211albidv 1924 . 2 (𝐴𝐶 → (∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐶𝐵))))
13 disj1 4448 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
14 dfss2 3966 . 2 (𝐴 ⊆ (𝐶𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐶𝐵)))
1512, 13, 143bitr4g 314 1 (𝐴𝐶 → ((𝐴𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wal 1540   = wceq 1542  wcel 2107  cdif 3943  cin 3945  wss 3946  c0 4320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-dif 3949  df-in 3953  df-ss 3963  df-nul 4321
This theorem is referenced by:  disj2  4455  ssdifsn  4787  oacomf1olem  8552  domdifsn  9042  elfiun  9412  cantnfp1lem3  9662  ssxr  11270  structcnvcnv  17073  fidomndrng  20900  elcls  22546  ist1-2  22820  nrmsep2  22829  nrmsep  22830  isnrm3  22832  isreg2  22850  hauscmplem  22879  connsub  22894  iunconnlem  22900  llycmpkgen2  23023  hausdiag  23118  trfil3  23361  isufil2  23381  filufint  23393  blcld  23983  i1fima2  25165  i1fd  25167  nbgrssvwo2  28586  pliguhgr  29704  symgcom2  32216  inunissunidif  36161  poimirlem15  36408  itg2addnclem2  36445  ntrk0kbimka  42661  ntrneicls11  42712  gneispace  42756  opndisj  47375  seposep  47398
  Copyright terms: Public domain W3C validator