MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unssd Structured version   Unicode version

Theorem unssd 3515
Description: A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
unssd.1  |-  ( ph  ->  A  C_  C )
unssd.2  |-  ( ph  ->  B  C_  C )
Assertion
Ref Expression
unssd  |-  ( ph  ->  ( A  u.  B
)  C_  C )

Proof of Theorem unssd
StepHypRef Expression
1 unssd.1 . 2  |-  ( ph  ->  A  C_  C )
2 unssd.2 . 2  |-  ( ph  ->  B  C_  C )
3 unss 3513 . . 3  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
43biimpi 187 . 2  |-  ( ( A  C_  C  /\  B  C_  C )  -> 
( A  u.  B
)  C_  C )
51, 2, 4syl2anc 643 1  |-  ( ph  ->  ( A  u.  B
)  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    u. cun 3310    C_ wss 3312
This theorem is referenced by:  tpssi  3957  fr3nr  4752  suceloni  4785  sofld  5310  marypha1lem  7430  wemapso2  7513  unwf  7728  rankunb  7768  ackbij1lem6  8097  ackbij1lem16  8107  ssfin4  8182  isfin1-3  8258  ttukeylem7  8387  fpwwe2lem13  8509  wuncval2  8614  inar1  8642  un0addcl  10245  un0mulcl  10246  fzosplit  11158  fzouzsplit  11160  hashf1lem1  11696  saddisj  12969  prmreclem5  13280  4sqlem11  13315  4sqlem19  13323  vdwlem1  13341  vdwlem12  13352  ramub1lem1  13386  ramub1lem2  13387  mrieqvlemd  13846  mreexmrid  13860  mreexexlem2d  13862  mreexexlem3d  13863  mreexexlem4d  13864  acsfiindd  14595  tsrdir  14675  lsmunss  15284  efgsfo  15363  gsumzaddlem  15518  lsptpcl  16047  lspun  16055  lsmsp  16150  lspsolvlem  16206  lspsolv  16207  lsppratlem3  16213  lsppratlem4  16214  islbs3  16219  lbsextlem4  16225  aspval2  16397  clslp  17204  neitr  17236  ordtuni  17246  ordtbas2  17247  ordtbas  17248  ordtrest  17258  cmpcld  17457  1stckgenlem  17577  1stckgen  17578  ptbasfi  17605  fbun  17864  trfil2  17911  isufil2  17932  ufileu  17943  filufint  17944  fmfnfm  17982  hausflim  18005  flimclslem  18008  fclsfnflim  18051  flimfnfcls  18052  alexsubALTlem3  18072  alexsubALTlem4  18073  tsmsgsum  18160  tsmsres  18165  tsmsxplem1  18174  ustund  18243  trust  18251  ustuqtop1  18263  prdsdsf  18389  prdsxmetlem  18390  prdsmet  18392  prdsbl  18513  prdsxmslem2  18551  restmetu  18609  icccmplem2  18846  ovolunlem1  19385  ovolunnul  19388  nulmbl2  19423  volun  19431  volcn  19490  itgsplitioo  19721  limcvallem  19750  limcdif  19755  ellimc2  19756  limcres  19765  limccnp  19770  limccnp2  19771  limcco  19772  dvreslem  19788  dvres2lem  19789  dvaddbr  19816  dvmulbr  19817  lhop2  19891  dvcnvrelem2  19894  evlseu  19929  elply2  20107  plyf  20109  elplyr  20112  elplyd  20113  ply1term  20115  ply0  20119  plyeq0lem  20121  plyeq0  20122  plyaddlem  20126  plymullem  20127  dgrlem  20140  coeidlem  20148  plyco  20152  plycj  20187  aannenlem2  20238  xrlimcnp  20799  perfectlem2  21006  shlej1  22854  shlub  22908  erdszelem8  24876  relexpfld  25129  dftrpred3g  25503  ftc1anclem7  26276  ftc1anc  26278  comppfsc  26378  topjoin  26385  prdsbnd  26493  rrnequiv  26535  ralxpmap  26733  elrfi  26739  cmpfiiin  26742  istopclsd  26745  mzpcompact2lem  26799  eldioph2lem2  26810  eldioph2  26811  rngunsnply  27346  f1omvdco2  27359  symgsssg  27376  symggen  27379  idomsubgmo  27482  bnj1136  29303  bnj1452  29358  pclfinN  30634  dochdmj1  32125  djhspss  32141  djhunssN  32144  djhlsmcl  32149  dvh4dimlem  32178  dvhdimlem  32179  lclkrlem2c  32244  lclkrlem2v  32263  mapdh9a  32525  hdmapval0  32571  hdmapval3lemN  32575  hdmap10lem  32577
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator