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

Theorem ssundif 4196
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 989 . . . 4 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) → 𝑥𝐶) ↔ (𝑥𝐴 → (𝑥𝐵𝑥𝐶)))
2 eldif 3725 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
32imbi1i 338 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ((𝑥𝐴 ∧ ¬ 𝑥𝐵) → 𝑥𝐶))
4 elun 3896 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
54imbi2i 325 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 → (𝑥𝐵𝑥𝐶)))
61, 3, 53bitr4ri 293 . . 3 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
76albii 1896 . 2 (∀𝑥(𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
8 dfss2 3732 . 2 (𝐴 ⊆ (𝐵𝐶) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐵𝐶)))
9 dfss2 3732 . 2 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
107, 8, 93bitr4i 292 1 (𝐴 ⊆ (𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  wal 1630  wcel 2139  cdif 3712  cun 3713  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729
This theorem is referenced by:  difcom  4197  uneqdifeq  4201  uneqdifeqOLD  4202  ssunsn2  4504  elpwun  7143  soex  7275  ressuppssdif  7485  frfi  8372  cantnfp1lem3  8752  dfacfin7  9433  zornn0g  9539  fpwwe2lem13  9676  hashbclem  13448  incexclem  14787  ramub1lem1  15952  lpcls  21390  cmpcld  21427  alexsubALTlem3  22074  restmetu  22596  uniiccdif  23566  abelthlem2  24405  abelthlem3  24406  imadifss  33715  frege124d  38573
  Copyright terms: Public domain W3C validator