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

Theorem ssundif 4004
 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 949 . . . 4 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) → 𝑥𝐶) ↔ (𝑥𝐴 → (𝑥𝐵𝑥𝐶)))
2 eldif 3550 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
32imbi1i 338 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ((𝑥𝐴 ∧ ¬ 𝑥𝐵) → 𝑥𝐶))
4 elun 3715 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
54imbi2i 325 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 → (𝑥𝐵𝑥𝐶)))
61, 3, 53bitr4ri 292 . . 3 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
76albii 1737 . 2 (∀𝑥(𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
8 dfss2 3557 . 2 (𝐴 ⊆ (𝐵𝐶) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐵𝐶)))
9 dfss2 3557 . 2 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
107, 8, 93bitr4i 291 1 (𝐴 ⊆ (𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383  ∀wal 1473   ∈ wcel 1977   ∖ cdif 3537   ∪ cun 3538   ⊆ wss 3540 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554 This theorem is referenced by:  difcom  4005  uneqdifeq  4009  uneqdifeqOLD  4010  ssunsn2  4299  elpwun  6869  soex  7002  ressuppssdif  7203  frfi  8090  cantnfp1lem3  8460  dfacfin7  9104  zornn0g  9210  fpwwe2lem13  9343  hashbclem  13093  incexclem  14407  ramub1lem1  15568  lpcls  20978  cmpcld  21015  alexsubALTlem3  21663  restmetu  22185  uniiccdif  23152  abelthlem2  23990  abelthlem3  23991  imadifss  32554  frege124d  37072
 Copyright terms: Public domain W3C validator