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

Theorem unss1 3815
 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 3630 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21orim1d 902 . . 3 (𝐴𝐵 → ((𝑥𝐴𝑥𝐶) → (𝑥𝐵𝑥𝐶)))
3 elun 3786 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elun 3786 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43imtr4g 285 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐴𝐶) → 𝑥 ∈ (𝐵𝐶)))
65ssrdv 3642 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 382   ∈ wcel 2030   ∪ cun 3605   ⊆ wss 3607 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-in 3614  df-ss 3621 This theorem is referenced by:  unss2  3817  unss12  3818  eldifpw  7018  tposss  7398  dftpos4  7416  hashbclem  13274  incexclem  14612  mreexexlem2d  16352  catcoppccl  16805  neitr  21032  restntr  21034  leordtval2  21064  cmpcld  21253  uniioombllem3  23399  limcres  23695  plyss  24000  shlej1  28347  ss2mcls  31591  orderseqlem  31877  noetalem4  31991  bj-rrhatsscchat  33253  pclfinclN  35554
 Copyright terms: Public domain W3C validator