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

Theorem unss1 3743
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 3561 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21orim1d 879 . . 3 (𝐴𝐵 → ((𝑥𝐴𝑥𝐶) → (𝑥𝐵𝑥𝐶)))
3 elun 3714 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elun 3714 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43imtr4g 283 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐴𝐶) → 𝑥 ∈ (𝐵𝐶)))
65ssrdv 3573 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 381  wcel 1976  cun 3537  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-in 3546  df-ss 3553
This theorem is referenced by:  unss2  3745  unss12  3746  eldifpw  6845  tposss  7217  dftpos4  7235  hashbclem  13045  incexclem  14353  mreexexlem2d  16074  catcoppccl  16527  neitr  20736  restntr  20738  leordtval2  20768  cmpcld  20957  uniioombllem3  23076  limcres  23373  plyss  23676  shlej1  27409  ss2mcls  30525  orderseqlem  30799  bj-rrhatsscchat  32096  pclfinclN  34050
  Copyright terms: Public domain W3C validator