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

Theorem ssundif 4391
 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 999 . . . 4 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) → 𝑥𝐶) ↔ (𝑥𝐴 → (𝑥𝐵𝑥𝐶)))
2 eldif 3891 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
32imbi1i 353 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ((𝑥𝐴 ∧ ¬ 𝑥𝐵) → 𝑥𝐶))
4 elun 4076 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
54imbi2i 339 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 → (𝑥𝐵𝑥𝐶)))
61, 3, 53bitr4ri 307 . . 3 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
76albii 1821 . 2 (∀𝑥(𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
8 dfss2 3901 . 2 (𝐴 ⊆ (𝐵𝐶) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐵𝐶)))
9 dfss2 3901 . 2 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
107, 8, 93bitr4i 306 1 (𝐴 ⊆ (𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844  ∀wal 1536   ∈ wcel 2111   ∖ cdif 3878   ∪ cun 3879   ⊆ wss 3881 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-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898 This theorem is referenced by:  difcom  4392  uneqdifeq  4396  ssunsn2  4720  elpwun  7473  soex  7610  ressuppssdif  7836  frfi  8749  cantnfp1lem3  9129  dfacfin7  9812  zornn0g  9918  fpwwe2lem12  10055  hashbclem  13808  incexclem  15185  ramub1lem1  16354  lpcls  21976  cmpcld  22014  alexsubALTlem3  22661  restmetu  23184  uniiccdif  24189  abelthlem2  25034  abelthlem3  25035  pmtrcnelor  30792  imadifss  35048  frege124d  40477
 Copyright terms: Public domain W3C validator