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

Theorem unss1 3744
 Description: Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
unss1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))

Proof of Theorem unss1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ssel 3562 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21orim1d 880 . . 3 (𝐴𝐵 → ((𝑥𝐴𝑥𝐶) → (𝑥𝐵𝑥𝐶)))
3 elun 3715 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elun 3715 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43imtr4g 284 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐴𝐶) → 𝑥 ∈ (𝐵𝐶)))
65ssrdv 3574 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 382   ∈ wcel 1977   ∪ 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-un 3545  df-in 3547  df-ss 3554 This theorem is referenced by:  unss2  3746  unss12  3747  eldifpw  6868  tposss  7240  dftpos4  7258  hashbclem  13093  incexclem  14407  mreexexlem2d  16128  catcoppccl  16581  neitr  20794  restntr  20796  leordtval2  20826  cmpcld  21015  uniioombllem3  23159  limcres  23456  plyss  23759  shlej1  27603  ss2mcls  30719  orderseqlem  30993  bj-rrhatsscchat  32300  pclfinclN  34254
 Copyright terms: Public domain W3C validator