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

Theorem ssun2 3339
Description: Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
ssun2  |-  A  C_  ( B  u.  A
)

Proof of Theorem ssun2
StepHypRef Expression
1 ssun1 3338 . 2  |-  A  C_  ( A  u.  B
)
2 uncom 3319 . 2  |-  ( A  u.  B )  =  ( B  u.  A
)
31, 2sseqtri 3210 1  |-  A  C_  ( B  u.  A
)
Colors of variables: wff set class
Syntax hints:    u. cun 3150    C_ wss 3152
This theorem is referenced by:  ssun4  3341  elun2  3343  nsspssun  3402  unv  3482  un00  3490  snsspr2  3765  snsstp3  3768  unexb  4520  difex2  4525  rnexg  4940  fvrn0  5550  fnsuppres  5732  brtpos0  6241  riotassuni  6343  oaabs2  6643  ertr  6675  domunsncan  6962  mapunen  7030  ac6sfi  7101  unfir  7125  domunfican  7129  iunfi  7144  finsschain  7162  elfiun  7183  dffi3  7184  hartogslem1  7257  unwdomg  7298  unxpwdom2  7302  unxpwdom  7303  trcl  7410  unwf  7482  rankunb  7522  r0weon  7640  infxpenlem  7641  alephfplem4  7734  cda1dif  7802  cdainflem  7817  infcda  7834  ackbij1lem16  7861  cfsuc  7883  fin1a2lem10  8035  axdc3lem4  8079  ttukeylem7  8142  fpwwe2lem13  8264  canthp1lem2  8275  gchac  8295  wunfi  8343  wunrn  8351  wunex2  8360  inar1  8397  ltrelxr  8886  un0mulcl  9998  pnfxr  10455  hashbclem  11390  hashf1lem1  11393  hashf1lem2  11394  ccatfn  11427  fsumsplit  12212  sumsplit  12231  fsum2dlem  12233  fsumabs  12259  fsumrlim  12269  fsumo1  12270  o1fsum  12271  fsumiun  12279  incexclem  12295  vdwlem5  13032  vdwlem8  13035  ramcl2  13063  srnginvl  13267  lmodvsca  13276  algsca  13281  algvsca  13282  phlvsca  13291  phlip  13292  odrngtset  13315  odrngle  13316  odrngds  13317  prdssca  13356  prdsvsca  13360  prdsle  13361  prdsds  13363  prdstset  13365  prdshom  13366  prdsco  13367  imasds  13416  imassca  13422  imasvsca  13423  imastset  13424  imasle  13425  mreexexlemd  13546  mreexexlem2d  13547  mreexexlem3d  13548  yonedalem1  14046  yonedalem21  14047  yonedalem3a  14048  yonedalem4c  14051  yonedalem22  14052  yonedalem3b  14053  yonedainv  14055  yonffthlem  14056  drsdirfi  14072  ipolerval  14259  psdmrn  14316  dirge  14359  gsumzaddlem  15203  gsumzsplit  15206  gsumsplit2  15208  gsum2d  15223  dprdfadd  15255  dmdprdsplit2lem  15280  dmdprdsplit2  15281  dmdprdsplit  15282  dprdsplit  15283  ablfac1eulem  15307  pgpfaclem1  15316  lspun  15744  lsmsp  15839  lsppratlem3  15902  lbsextlem2  15912  lbsextlem3  15913  lbsextlem4  15914  psrbagaddcl  16116  psrsca  16134  psrvscafval  16135  mplsubglem  16179  mplcoe1  16209  mplcoe2  16211  opsrtoslem2  16226  cnfldcj  16386  cnfldtset  16387  cnfldle  16388  cnfldds  16389  ordtbas2  16921  ordtbas  16922  ordtopn1  16924  ordtopn2  16925  leordtval2  16942  icomnfordt  16946  iooordt  16947  perfcls  17093  uncmp  17130  fiuncmp  17131  2ndcdisj2  17183  1stckgenlem  17248  1stckgen  17249  ptbasin  17272  ptbasfi  17276  dfac14lem  17311  dfac14  17312  ptuncnv  17498  ptunhmeo  17499  ptcmpfi  17504  fbun  17535  filcon  17578  isufil2  17603  ufprim  17604  filufint  17615  fin1aufil  17627  fmfnfmlem4  17652  hausflim  17676  flimclslem  17679  fclsfnflim  17722  flimfnfcls  17723  tmdgsum  17778  tsmsgsum  17821  tsmssplit  17834  tsmsxplem1  17835  prdsdsf  17931  prdsmet  17934  prdsbl  18037  fsumcn  18374  cnmpt2pc  18426  ovolctb2  18851  ovolfiniun  18860  finiunmbl  18901  volfiniun  18904  uniioombllem3  18940  uniioombllem4  18941  mbfres2  19000  itg2splitlem  19103  itg2split  19104  itgfsum  19181  itgsplit  19190  limcvallem  19221  ellimc2  19227  limccnp  19241  limccnp2  19242  limcco  19243  dvmptfsum  19322  lhop2  19362  lhop  19363  mdegcl  19455  elply2  19578  elplyd  19584  ply1term  19586  ply0  19590  plyaddlem1  19595  plymullem1  19596  plymullem  19598  mtest  19781  xrlimcnp  20263  jensenlem1  20281  jensenlem2  20282  jensen  20283  fsumharmonic  20305  chtdif  20396  lgsdir2lem3  20564  lgsquadlem2  20594  dchrisumlem2  20639  dchrisum0lem1b  20664  dchrisum0lem1  20665  pntrlog2bndlem6  20732  pntlemf  20754  shsleji  21949  shsval2i  21966  ssjo  22026  sshhococi  22125  subfacp1lem2a  23122  subfacp1lem3  23124  subfacp1lem5  23126  erdszelem8  23140  kur14lem7  23154  cvmliftlem10  23236  eupap1  23311  wfrlem14  23680  wfrlem16  23682  nofulllem4  23770  ranfldrefc  24470  refssfne  25706  comppfsc  25719  topjoin  25726  tailf  25736  prdsbnd  25929  heibor1lem  25945  mzpcompact2lem  26241  eldioph2  26253  eldioph4b  26306  ttac  26541  pwssplit4  26603  isnumbasgrplem2  26681  isnumbasabl  26683  dfacbasgrp  26685  rngunsnply  26790  fiuneneq  26925  bnj970  28352  bnj1137  28398  sspadd2  29378  pclfinN  29462  dochdmj1  30953
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