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

Theorem unss1 4098
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 3898 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21orim1d 966 . . 3 (𝐴𝐵 → ((𝑥𝐴𝑥𝐶) → (𝑥𝐵𝑥𝐶)))
3 elun 4068 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elun 4068 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43imtr4g 299 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐴𝐶) → 𝑥 ∈ (𝐵𝐶)))
65ssrdv 3912 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 847  wcel 2110  cun 3869  wss 3871
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3415  df-un 3876  df-in 3878  df-ss 3888
This theorem is referenced by:  unss2  4100  unss12  4101  eldifpw  7558  tposss  7974  dftpos4  7992  hashbclem  14021  incexclem  15405  mreexexlem2d  17153  catcoppccl  17628  catcoppcclOLD  17629  neitr  22082  restntr  22084  leordtval2  22114  cmpcld  22304  uniioombllem3  24487  limcres  24788  plyss  25098  shlej1  29446  fineqvac  32784  ss2mcls  33248  orderseqlem  33543  bj-rrhatsscchat  35147  pclfinclN  37706
  Copyright terms: Public domain W3C validator