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

Theorem ssundif 4445
Description: A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007.)
Assertion
Ref Expression
ssundif (𝐴 ⊆ (𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)

Proof of Theorem ssundif
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 pm5.6 1000 . . . 4 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) → 𝑥𝐶) ↔ (𝑥𝐴 → (𝑥𝐵𝑥𝐶)))
2 eldif 3920 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
32imbi1i 349 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ((𝑥𝐴 ∧ ¬ 𝑥𝐵) → 𝑥𝐶))
4 elun 4108 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
54imbi2i 335 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 → (𝑥𝐵𝑥𝐶)))
61, 3, 53bitr4ri 303 . . 3 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
76albii 1821 . 2 (∀𝑥(𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
8 dfss2 3930 . 2 (𝐴 ⊆ (𝐵𝐶) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐵𝐶)))
9 dfss2 3930 . 2 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
107, 8, 93bitr4i 302 1 (𝐴 ⊆ (𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  wal 1539  wcel 2106  cdif 3907  cun 3908  wss 3910
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927
This theorem is referenced by:  difcom  4446  uneqdifeq  4450  ssunsn2  4787  elpwun  7703  soex  7858  ressuppssdif  8116  ssfi  9117  frfi  9232  cantnfp1lem3  9616  dfacfin7  10335  zornn0g  10441  fpwwe2lem12  10578  hashbclem  14349  incexclem  15721  ramub1lem1  16898  lpcls  22715  cmpcld  22753  alexsubALTlem3  23400  restmetu  23926  uniiccdif  24942  abelthlem2  25791  abelthlem3  25792  pmtrcnelor  31942  imadifss  36053  frege124d  42023
  Copyright terms: Public domain W3C validator