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

Theorem reldisj 4362
 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 2175. (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 3903 . . . 4 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
2 eleq1w 2872 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
3 eleq1w 2872 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝐶𝑦𝐶))
42, 3imbi12d 348 . . . . . 6 (𝑥 = 𝑦 → ((𝑥𝐴𝑥𝐶) ↔ (𝑦𝐴𝑦𝐶)))
54spw 2041 . . . . 5 (∀𝑥(𝑥𝐴𝑥𝐶) → (𝑥𝐴𝑥𝐶))
6 pm5.44 546 . . . . . 6 ((𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴 → (𝑥𝐶 ∧ ¬ 𝑥𝐵))))
7 eldif 3893 . . . . . . 7 (𝑥 ∈ (𝐶𝐵) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐵))
87imbi2i 339 . . . . . 6 ((𝑥𝐴𝑥 ∈ (𝐶𝐵)) ↔ (𝑥𝐴 → (𝑥𝐶 ∧ ¬ 𝑥𝐵)))
96, 8bitr4di 292 . . . . 5 ((𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
105, 9syl 17 . . . 4 (∀𝑥(𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
111, 10sylbi 220 . . 3 (𝐴𝐶 → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
1211albidv 1921 . 2 (𝐴𝐶 → (∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐶𝐵))))
13 disj1 4361 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
14 dfss2 3903 . 2 (𝐴 ⊆ (𝐶𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐶𝐵)))
1512, 13, 143bitr4g 317 1 (𝐴𝐶 → ((𝐴𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶𝐵)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538   ∈ wcel 2111   ∖ cdif 3880   ∩ cin 3882   ⊆ wss 3883  ∅c0 4246 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-v 3444  df-dif 3886  df-in 3890  df-ss 3900  df-nul 4247 This theorem is referenced by:  disj2  4368  ssdifsn  4684  oacomf1olem  8191  domdifsn  8601  elfiun  8896  cantnfp1lem3  9145  ssxr  10717  structcnvcnv  16509  fidomndrng  20094  elcls  21719  ist1-2  21993  nrmsep2  22002  nrmsep  22003  isnrm3  22005  isreg2  22023  hauscmplem  22052  connsub  22067  iunconnlem  22073  llycmpkgen2  22196  hausdiag  22291  trfil3  22534  isufil2  22554  filufint  22566  blcld  23153  i1fima2  24324  i1fd  24326  nbgrssvwo2  27196  pliguhgr  28313  symgcom2  30827  inunissunidif  34943  poimirlem15  35223  itg2addnclem2  35260  ntrk0kbimka  40913  ntrneicls11  40964  gneispace  41008
 Copyright terms: Public domain W3C validator