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

Theorem unss1 4184
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 3976 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21orim1d 967 . . 3 (𝐴𝐵 → ((𝑥𝐴𝑥𝐶) → (𝑥𝐵𝑥𝐶)))
3 elun 4152 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elun 4152 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43imtr4g 296 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐴𝐶) → 𝑥 ∈ (𝐵𝐶)))
65ssrdv 3988 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 847  wcel 2107  cun 3948  wss 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955  df-ss 3967
This theorem is referenced by:  unss2  4186  unss12  4187  eldifpw  7789  orderseqlem  8183  tposss  8253  dftpos4  8271  hashbclem  14492  incexclem  15873  mreexexlem2d  17689  catcoppccl  18163  neitr  23189  restntr  23191  leordtval2  23221  cmpcld  23411  uniioombllem3  25621  limcres  25922  plyss  26239  mulsproplem13  28155  mulsproplem14  28156  shlej1  31380  fineqvac  35112  ss2mcls  35574  bj-rrhatsscchat  37238  pclfinclN  39953  dmtposss  48782
  Copyright terms: Public domain W3C validator