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

Theorem unssd 3525
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 3523 . . 3  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
43biimpi 188 . 2  |-  ( ( A  C_  C  /\  B  C_  C )  -> 
( A  u.  B
)  C_  C )
51, 2, 4syl2anc 644 1  |-  ( ph  ->  ( A  u.  B
)  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    u. cun 3320    C_ wss 3322
This theorem is referenced by:  tpssi  3967  fr3nr  4763  suceloni  4796  sofld  5321  marypha1lem  7441  wemapso2  7524  unwf  7739  rankunb  7779  ackbij1lem6  8110  ackbij1lem16  8120  ssfin4  8195  isfin1-3  8271  ttukeylem7  8400  fpwwe2lem13  8522  wuncval2  8627  inar1  8655  un0addcl  10258  un0mulcl  10259  fzosplit  11171  fzouzsplit  11173  hashf1lem1  11709  saddisj  12982  prmreclem5  13293  4sqlem11  13328  4sqlem19  13336  vdwlem1  13354  vdwlem12  13365  ramub1lem1  13399  ramub1lem2  13400  mrieqvlemd  13859  mreexmrid  13873  mreexexlem2d  13875  mreexexlem3d  13876  mreexexlem4d  13877  acsfiindd  14608  tsrdir  14688  lsmunss  15297  efgsfo  15376  gsumzaddlem  15531  lsptpcl  16060  lspun  16068  lsmsp  16163  lspsolvlem  16219  lspsolv  16220  lsppratlem3  16226  lsppratlem4  16227  islbs3  16232  lbsextlem4  16238  aspval2  16410  clslp  17217  neitr  17249  ordtuni  17259  ordtbas2  17260  ordtbas  17261  ordtrest  17271  cmpcld  17470  1stckgenlem  17590  1stckgen  17591  ptbasfi  17618  fbun  17877  trfil2  17924  isufil2  17945  ufileu  17956  filufint  17957  fmfnfm  17995  hausflim  18018  flimclslem  18021  fclsfnflim  18064  flimfnfcls  18065  alexsubALTlem3  18085  alexsubALTlem4  18086  tsmsgsum  18173  tsmsres  18178  tsmsxplem1  18187  ustund  18256  trust  18264  ustuqtop1  18276  prdsdsf  18402  prdsxmetlem  18403  prdsmet  18405  prdsbl  18526  prdsxmslem2  18564  restmetu  18622  icccmplem2  18859  ovolunlem1  19398  ovolunnul  19401  nulmbl2  19436  volun  19444  volcn  19503  itgsplitioo  19732  limcvallem  19763  limcdif  19768  ellimc2  19769  limcres  19778  limccnp  19783  limccnp2  19784  limcco  19785  dvreslem  19801  dvres2lem  19802  dvaddbr  19829  dvmulbr  19830  lhop2  19904  dvcnvrelem2  19907  evlseu  19942  elply2  20120  plyf  20122  elplyr  20125  elplyd  20126  ply1term  20128  ply0  20132  plyeq0lem  20134  plyeq0  20135  plyaddlem  20139  plymullem  20140  dgrlem  20153  coeidlem  20161  plyco  20165  plycj  20200  aannenlem2  20251  xrlimcnp  20812  perfectlem2  21019  shlej1  22867  shlub  22921  erdszelem8  24889  relexpfld  25142  dftrpred3g  25516  ftc1anclem7  26300  ftc1anc  26302  comppfsc  26401  topjoin  26408  prdsbnd  26516  rrnequiv  26558  ralxpmap  26756  elrfi  26762  cmpfiiin  26765  istopclsd  26768  mzpcompact2lem  26822  eldioph2lem2  26833  eldioph2  26834  rngunsnply  27369  f1omvdco2  27382  symgsssg  27399  symggen  27402  idomsubgmo  27505  bnj1136  29440  bnj1452  29495  pclfinN  30771  dochdmj1  32262  djhspss  32278  djhunssN  32281  djhlsmcl  32286  dvh4dimlem  32315  dvhdimlem  32316  lclkrlem2c  32381  lclkrlem2v  32400  mapdh9a  32662  hdmapval0  32708  hdmapval3lemN  32712  hdmap10lem  32714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator