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

Theorem unssd 3351
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 3349 . . 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 3150    C_ wss 3152
This theorem is referenced by:  fr3nr  4571  suceloni  4604  sofld  5121  marypha1lem  7186  wemapso2  7267  unwf  7482  rankunb  7522  ackbij1lem6  7851  ackbij1lem16  7861  ssfin4  7936  isfin1-3  8012  ttukeylem7  8142  fpwwe2lem13  8264  wuncval2  8369  inar1  8397  un0addcl  9997  un0mulcl  9998  fzosplit  10899  fzouzsplit  10901  hashf1lem1  11393  saddisj  12656  prmreclem5  12967  4sqlem11  13002  4sqlem19  13010  vdwlem1  13028  vdwlem12  13039  ramub1lem1  13073  ramub1lem2  13074  mrieqvlemd  13531  mreexmrid  13545  mreexexlem2d  13547  mreexexlem3d  13548  mreexexlem4d  13549  acsfiindd  14280  tsrdir  14360  lsmunss  14969  efgsfo  15048  gsumzaddlem  15203  lsptpcl  15736  lspun  15744  lsmsp  15839  lspsolvlem  15895  lspsolv  15896  lsppratlem3  15902  lsppratlem4  15903  islbs3  15908  lbsextlem4  15914  aspval2  16086  clslp  16879  ordtuni  16920  ordtbas2  16921  ordtbas  16922  ordtrest  16932  cmpcld  17129  1stckgenlem  17248  1stckgen  17249  ptbasfi  17276  fbun  17535  trfil2  17582  isufil2  17603  ufileu  17614  filufint  17615  fmfnfm  17653  hausflim  17676  flimclslem  17679  fclsfnflim  17722  flimfnfcls  17723  alexsubALTlem3  17743  alexsubALTlem4  17744  tsmsgsum  17821  tsmsres  17826  tsmsxplem1  17835  prdsdsf  17931  prdsxmetlem  17932  prdsmet  17934  prdsbl  18037  prdsxmslem2  18075  icccmplem2  18328  ovolunlem1  18856  ovolunnul  18859  nulmbl2  18894  volun  18902  volcn  18961  itgsplitioo  19192  limcvallem  19221  limcdif  19226  ellimc2  19227  limcres  19236  limccnp  19241  limccnp2  19242  limcco  19243  dvreslem  19259  dvres2lem  19260  dvaddbr  19287  dvmulbr  19288  lhop2  19362  dvcnvrelem2  19365  evlseu  19400  elply2  19578  plyf  19580  elplyr  19583  elplyd  19584  ply1term  19586  ply0  19590  plyeq0lem  19592  plyeq0  19593  plyaddlem  19597  plymullem  19598  dgrlem  19611  coeidlem  19619  plyco  19623  plycj  19658  aannenlem2  19709  xrlimcnp  20263  perfectlem2  20469  shlej1  21939  shlub  21993  erdszelem8  23729  relexpfld  24034  dftrpred3g  24236  cnfilca  25556  islimrs4  25582  pgapspf  26052  rayline  26156  comppfsc  26307  topjoin  26314  prdsbnd  26517  rrnequiv  26559  ralxpmap  26761  elrfi  26769  cmpfiiin  26772  istopclsd  26775  mzpcompact2lem  26829  eldioph2lem2  26840  eldioph2  26841  rngunsnply  27378  f1omvdco2  27391  symgsssg  27408  symggen  27411  idomsubgmo  27514  bnj1136  29027  bnj1452  29082  pclfinN  30089  dochdmj1  31580  djhspss  31596  djhunssN  31599  djhlsmcl  31604  dvh4dimlem  31633  dvhdimlem  31634  lclkrlem2c  31699  lclkrlem2v  31718  mapdh9a  31980  hdmapval0  32026  hdmapval3lemN  32030  hdmap10lem  32032
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator