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

Theorem ssun1 3338
Description: Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ssun1  |-  A  C_  ( A  u.  B
)

Proof of Theorem ssun1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 orc 374 . . 3  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
2 elun 3316 . . 3  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
31, 2sylibr 203 . 2  |-  ( x  e.  A  ->  x  e.  ( A  u.  B
) )
43ssriv 3184 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    \/ wo 357    e. wcel 1684    u. cun 3150    C_ wss 3152
This theorem is referenced by:  ssun2  3339  ssun3  3340  elun1  3342  inabs  3400  reuun1  3450  un00  3490  snsspr1  3764  snsstp1  3766  snsstp2  3767  uniintsn  3899  sssucid  4469  unexb  4520  dmexg  4939  sofld  5121  fvrn0  5550  dftpos2  6251  tpostpos2  6255  riotassuni  6343  tfrlem11  6404  oaabs2  6643  ersym  6672  domss2  7020  mapunen  7030  ac6sfi  7101  frfi  7102  unfir  7125  domunfican  7129  iunfi  7144  finsschain  7162  elfiun  7183  dffi3  7184  unwdomg  7298  unxpwdom2  7302  unxpwdom  7303  cantnfp1lem1  7380  cantnfp1lem3  7382  tc2  7427  unwf  7482  rankunb  7522  r0weon  7640  infxpenlem  7641  dfac2  7757  cdadom3  7814  cdainflem  7817  infunabs  7833  infcda  7834  infdif  7835  ackbij1lem15  7860  ackbij1lem16  7861  cfsmolem  7896  isfin4-3  7941  fin23lem11  7943  fin1a2lem10  8035  fin1a2lem13  8038  axdc3lem4  8079  axcclem  8083  zornn0g  8132  ttukeylem1  8136  ttukeylem5  8140  ttukeylem7  8142  fingch  8245  fpwwe2lem13  8264  gchac  8295  wunfi  8343  wundm  8350  wunex2  8360  inar1  8397  ressxr  8876  nnssnn0  9968  un0addcl  9997  un0mulcl  9998  hashbclem  11390  hashf1lem1  11393  hashf1lem2  11394  ccatfn  11427  fsumsplit  12212  sumsplit  12231  fsum2d  12234  fsumabs  12259  fsumrlim  12269  fsumo1  12270  fsumiun  12279  incexclem  12295  vdwapid1  13022  vdwlem6  13033  ramcl2  13063  isstruct2  13157  srngbase  13264  srngplusg  13265  srngmulr  13266  lmodbase  13273  lmodplusg  13274  lmodsca  13275  algbase  13278  algaddg  13279  algmulr  13280  phlbase  13288  phlplusg  13289  phlsca  13290  odrngbas  13312  odrngplusg  13313  odrngmulr  13314  prdssca  13356  prdsbas  13357  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  prdsle  13361  prdsds  13363  prdstset  13365  imasbas  13415  imasplusg  13420  imasmulr  13421  imassca  13422  imasvsca  13423  mreexexlem2d  13547  yonedalem1  14046  yonedalem21  14047  yonedalem22  14052  yonffthlem  14056  drsdirfi  14072  ipobas  14258  ipotset  14260  acsfiindd  14280  psdmrn  14316  dirdm  14356  gsumzaddlem  15203  gsumzsplit  15206  gsumsplit2  15208  gsum2d  15223  dprdfadd  15255  dmdprdsplit2lem  15280  dmdprdsplit2  15281  dmdprdsplit  15282  dprdsplit  15283  ablfac1eulem  15307  lspun  15744  lsmsp  15839  lspsolv  15896  lsppratlem3  15902  islbs3  15908  lbsextlem2  15912  lbsextlem4  15914  psrbagaddcl  16116  psrbas  16124  psrplusg  16126  psrmulr  16129  mplsubglem  16179  mplcoe1  16209  mplcoe2  16211  cnfldbas  16383  cnfldadd  16384  cnfldmul  16385  cnfldcj  16386  basdif0  16691  tgdif0  16730  ordtbas2  16921  ordtbas  16922  ordtopn1  16924  leordtval2  16942  iocpnfordt  16945  icomnfordt  16946  uncmp  17130  fiuncmp  17131  1stckgenlem  17248  1stckgen  17249  ptbasin  17272  ptbasfi  17276  dfac14lem  17311  dfac14  17312  ptuncnv  17498  ptunhmeo  17499  ptcmpfi  17504  fbun  17535  trfil2  17582  isufil2  17603  ufprim  17604  ufileu  17614  filufint  17615  ufildr  17626  fmfnfm  17653  hausflim  17676  flimclslem  17679  fclsfnflim  17722  flimfnfcls  17723  alexsubALTlem4  17744  tmdgsum  17778  tsmsgsum  17821  tsmsres  17826  tsmssplit  17834  tsmsxplem1  17835  prdsxmetlem  17932  imasdsf1olem  17937  prdsbl  18037  icccmplem2  18328  fsumcn  18374  cnmpt2pc  18426  iccpnfcnv  18442  ovolctb2  18851  ovolunnul  18859  ovolfiniun  18860  nulmbl2  18894  finiunmbl  18901  volfiniun  18904  icombl  18921  ioombl  18922  uniiccdif  18933  mbfres2  19000  itg2splitlem  19103  itg2split  19104  itgfsum  19181  itgsplit  19190  itgsplitioo  19192  limcdif  19226  dvreslem  19259  dvaddbr  19287  dvmulbr  19288  dvmptfsum  19322  lhop  19363  dvcnvrelem2  19365  mdegcl  19455  elplyr  19583  plyrem  19685  xrlimcnp  20263  jensenlem1  20281  jensenlem2  20282  jensen  20283  fsumharmonic  20305  chtdif  20396  lgsdir2lem3  20564  lgsquadlem2  20594  dchrisum0lem1b  20664  pntrlog2bndlem6  20732  pntlemf  20754  ex-ss  20814  shsleji  21949  shsval2i  21966  ssjo  22026  sshhococi  22125  esumsplit  23431  subfacp1lem2b  23712  subfacp1lem3  23713  subfacp1lem5  23715  kur14lem7  23743  kur14lem9  23745  cvmliftlem10  23825  dftrpred3g  24236  wfrlem14  24269  wfrlem15  24270  nofulllem4  24359  domfldrefc  25057  prl  25167  basexre  25522  islimrs4  25582  segray  26155  refssfne  26294  locfincmp  26304  comppfsc  26307  filnetlem3  26329  prdsbnd  26517  heibor1lem  26533  rrnequiv  26559  ralxpmap  26761  elrfi  26769  mzpcompact2lem  26829  eldioph2  26841  eldioph4b  26894  ttac  27129  pwssplit4  27191  pwslnmlem2  27195  isnumbasgrplem2  27269  rngunsnply  27378  fiuneneq  27513  idomsubgmo  27514  compne  27642  bnj931  28802  paddunssN  29997  sspadd1  30004  sspadd2  30005  pclfinN  30089  dochdmj1  31580  dvhdimlem  31634
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