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

Theorem unssd 3364
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 3362 . . 3  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
43biimpi 186 . 2  |-  ( ( A  C_  C  /\  B  C_  C )  -> 
( A  u.  B
)  C_  C )
51, 2, 4syl2anc 642 1  |-  ( ph  ->  ( A  u.  B
)  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    u. cun 3163    C_ wss 3165
This theorem is referenced by:  fr3nr  4587  suceloni  4620  sofld  5137  marypha1lem  7202  wemapso2  7283  unwf  7498  rankunb  7538  ackbij1lem6  7867  ackbij1lem16  7877  ssfin4  7952  isfin1-3  8028  ttukeylem7  8158  fpwwe2lem13  8280  wuncval2  8385  inar1  8413  un0addcl  10013  un0mulcl  10014  fzosplit  10915  fzouzsplit  10917  hashf1lem1  11409  saddisj  12672  prmreclem5  12983  4sqlem11  13018  4sqlem19  13026  vdwlem1  13044  vdwlem12  13055  ramub1lem1  13089  ramub1lem2  13090  mrieqvlemd  13547  mreexmrid  13561  mreexexlem2d  13563  mreexexlem3d  13564  mreexexlem4d  13565  acsfiindd  14296  tsrdir  14376  lsmunss  14985  efgsfo  15064  gsumzaddlem  15219  lsptpcl  15752  lspun  15760  lsmsp  15855  lspsolvlem  15911  lspsolv  15912  lsppratlem3  15918  lsppratlem4  15919  islbs3  15924  lbsextlem4  15930  aspval2  16102  clslp  16895  ordtuni  16936  ordtbas2  16937  ordtbas  16938  ordtrest  16948  cmpcld  17145  1stckgenlem  17264  1stckgen  17265  ptbasfi  17292  fbun  17551  trfil2  17598  isufil2  17619  ufileu  17630  filufint  17631  fmfnfm  17669  hausflim  17692  flimclslem  17695  fclsfnflim  17738  flimfnfcls  17739  alexsubALTlem3  17759  alexsubALTlem4  17760  tsmsgsum  17837  tsmsres  17842  tsmsxplem1  17851  prdsdsf  17947  prdsxmetlem  17948  prdsmet  17950  prdsbl  18053  prdsxmslem2  18091  icccmplem2  18344  ovolunlem1  18872  ovolunnul  18875  nulmbl2  18910  volun  18918  volcn  18977  itgsplitioo  19208  limcvallem  19237  limcdif  19242  ellimc2  19243  limcres  19252  limccnp  19257  limccnp2  19258  limcco  19259  dvreslem  19275  dvres2lem  19276  dvaddbr  19303  dvmulbr  19304  lhop2  19378  dvcnvrelem2  19381  evlseu  19416  elply2  19594  plyf  19596  elplyr  19599  elplyd  19600  ply1term  19602  ply0  19606  plyeq0lem  19608  plyeq0  19609  plyaddlem  19613  plymullem  19614  dgrlem  19627  coeidlem  19635  plyco  19639  plycj  19674  aannenlem2  19725  xrlimcnp  20279  perfectlem2  20485  shlej1  21955  shlub  22009  erdszelem8  23744  relexpfld  24049  dftrpred3g  24307  cnfilca  25659  islimrs4  25685  pgapspf  26155  rayline  26259  comppfsc  26410  topjoin  26417  prdsbnd  26620  rrnequiv  26662  ralxpmap  26864  elrfi  26872  cmpfiiin  26875  istopclsd  26878  mzpcompact2lem  26932  eldioph2lem2  26943  eldioph2  26944  rngunsnply  27481  f1omvdco2  27494  symgsssg  27511  symggen  27514  idomsubgmo  27617  bnj1136  29343  bnj1452  29398  pclfinN  30711  dochdmj1  32202  djhspss  32218  djhunssN  32221  djhlsmcl  32226  dvh4dimlem  32255  dvhdimlem  32256  lclkrlem2c  32321  lclkrlem2v  32340  mapdh9a  32602  hdmapval0  32648  hdmapval3lemN  32652  hdmap10lem  32654
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator