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

Theorem reldisj 4452
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 3969 . . . 4 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
2 eleq1w 2817 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
3 eleq1w 2817 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝐶𝑦𝐶))
42, 3imbi12d 345 . . . . . 6 (𝑥 = 𝑦 → ((𝑥𝐴𝑥𝐶) ↔ (𝑦𝐴𝑦𝐶)))
54spw 2038 . . . . 5 (∀𝑥(𝑥𝐴𝑥𝐶) → (𝑥𝐴𝑥𝐶))
6 pm5.44 544 . . . . . 6 ((𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴 → (𝑥𝐶 ∧ ¬ 𝑥𝐵))))
7 eldif 3959 . . . . . . 7 (𝑥 ∈ (𝐶𝐵) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐵))
87imbi2i 336 . . . . . 6 ((𝑥𝐴𝑥 ∈ (𝐶𝐵)) ↔ (𝑥𝐴 → (𝑥𝐶 ∧ ¬ 𝑥𝐵)))
96, 8bitr4di 289 . . . . 5 ((𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
105, 9syl 17 . . . 4 (∀𝑥(𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
111, 10sylbi 216 . . 3 (𝐴𝐶 → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
1211albidv 1924 . 2 (𝐴𝐶 → (∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐶𝐵))))
13 disj1 4451 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
14 dfss2 3969 . 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 3946  cin 3948  wss 3949  c0 4323
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 3952  df-in 3956  df-ss 3966  df-nul 4324
This theorem is referenced by:  disj2  4458  ssdifsn  4792  oacomf1olem  8564  domdifsn  9054  elfiun  9425  cantnfp1lem3  9675  ssxr  11283  structcnvcnv  17086  fidomndrng  20926  elcls  22577  ist1-2  22851  nrmsep2  22860  nrmsep  22861  isnrm3  22863  isreg2  22881  hauscmplem  22910  connsub  22925  iunconnlem  22931  llycmpkgen2  23054  hausdiag  23149  trfil3  23392  isufil2  23412  filufint  23424  blcld  24014  i1fima2  25196  i1fd  25198  nbgrssvwo2  28619  pliguhgr  29739  symgcom2  32245  inunissunidif  36256  poimirlem15  36503  itg2addnclem2  36540  ntrk0kbimka  42790  ntrneicls11  42841  gneispace  42885  opndisj  47535  seposep  47558
  Copyright terms: Public domain W3C validator