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

Theorem ssun1 3502
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 375 . . 3  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
2 elun 3480 . . 3  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
31, 2sylibr 204 . 2  |-  ( x  e.  A  ->  x  e.  ( A  u.  B
) )
43ssriv 3344 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    \/ wo 358    e. wcel 1725    u. cun 3310    C_ wss 3312
This theorem is referenced by:  ssun2  3503  ssun3  3504  elun1  3506  inabs  3564  reuun1  3615  un00  3655  snsspr1  3939  snsstp1  3941  snsstp2  3942  uniintsn  4079  sssucid  4650  unexb  4700  dmexg  5121  sofld  5309  fvrn0  5744  dftpos2  6487  tpostpos2  6491  riotassuni  6579  tfrlem11  6640  oaabs2  6879  domss2  7257  mapunen  7267  ac6sfi  7342  frfi  7343  unfir  7366  domunfican  7370  iunfi  7385  elfiun  7426  dffi3  7427  unwdomg  7541  unxpwdom2  7545  unxpwdom  7546  cantnfp1lem1  7623  cantnfp1lem3  7625  tc2  7670  unwf  7725  rankunb  7765  r0weon  7883  infxpenlem  7884  dfac2  8000  cdadom3  8057  cdainflem  8060  infunabs  8076  infcda  8077  infdif  8078  ackbij1lem15  8103  cfsmolem  8139  isfin4-3  8184  fin23lem11  8186  fin1a2lem10  8278  fin1a2lem13  8281  axdc3lem4  8322  axcclem  8326  zornn0g  8374  ttukeylem1  8378  ttukeylem5  8382  ttukeylem7  8384  fingch  8487  fpwwe2lem13  8506  gchac  8537  wunfi  8585  wundm  8592  wunex2  8602  inar1  8639  ressxr  9118  nnssnn0  10213  un0addcl  10242  un0mulcl  10243  hashbclem  11689  hashf1lem1  11692  hashf1lem2  11693  ccatfn  11729  fsumsplit  12521  fsum2d  12543  fsumabs  12568  fsumrlim  12578  fsumo1  12579  incexclem  12604  vdwapid1  13331  vdwlem6  13342  ramcl2  13372  isstruct2  13466  srngbase  13573  srngplusg  13574  srngmulr  13575  lmodbase  13582  lmodplusg  13583  lmodsca  13584  algbase  13587  algaddg  13588  algmulr  13589  phlbase  13597  phlplusg  13598  phlsca  13599  odrngbas  13623  odrngplusg  13624  odrngmulr  13625  prdssca  13667  prdsbas  13668  prdsplusg  13669  prdsmulr  13670  prdsvsca  13671  prdsle  13672  prdsds  13674  prdstset  13676  imasbas  13726  imasplusg  13731  imasmulr  13732  imassca  13733  imasvsca  13734  mreexexlem2d  13858  drsdirfi  14383  ipobas  14569  ipotset  14571  acsfiindd  14591  psdmrn  14627  dirdm  14667  gsumzaddlem  15514  gsumzsplit  15517  gsumsplit2  15519  gsum2d  15534  dprdfadd  15566  dmdprdsplit2lem  15591  dmdprdsplit2  15592  dmdprdsplit  15593  dprdsplit  15594  ablfac1eulem  15618  lspun  16051  lspsolv  16203  lsppratlem3  16209  islbs3  16215  lbsextlem2  16219  lbsextlem4  16221  psrbagaddcl  16423  psrbas  16431  psrplusg  16433  psrmulr  16436  mplsubglem  16486  mplcoe1  16516  mplcoe2  16518  cnfldbas  16695  cnfldadd  16696  cnfldmul  16697  cnfldcj  16698  cnfldtset  16699  cnfldle  16700  cnfldds  16701  basdif0  17006  tgdif0  17045  ordtbas2  17243  ordtbas  17244  ordtopn1  17246  leordtval2  17264  iocpnfordt  17267  icomnfordt  17268  uncmp  17454  fiuncmp  17455  1stckgenlem  17573  1stckgen  17574  ptbasin  17597  ptbasfi  17601  dfac14lem  17637  dfac14  17638  ptuncnv  17827  ptunhmeo  17828  ptcmpfi  17833  fbun  17860  trfil2  17907  ufprim  17929  ufileu  17939  filufint  17940  ufildr  17951  fmfnfm  17978  hausflim  18001  fclsfnflim  18047  alexsubALTlem4  18069  tmdgsum  18113  tsmsgsum  18156  tsmsres  18161  tsmssplit  18169  tsmsxplem1  18170  ustssco  18232  ustuqtop1  18259  prdsxmetlem  18386  prdsbl  18509  icccmplem2  18842  fsumcn  18888  cnmpt2pc  18941  iccpnfcnv  18957  ovolctb2  19376  ovolunnul  19384  ovolfiniun  19385  nulmbl2  19419  finiunmbl  19426  volfiniun  19429  icombl  19446  ioombl  19447  uniiccdif  19458  mbfres2  19525  itg2splitlem  19628  itg2split  19629  itgfsum  19706  itgsplit  19715  itgsplitioo  19717  dvreslem  19784  dvaddbr  19812  dvmulbr  19813  dvmptfsum  19847  lhop  19888  dvcnvrelem2  19890  mdegcl  19980  elplyr  20108  plyrem  20210  xrlimcnp  20795  fsumharmonic  20838  chtdif  20929  lgsdir2lem3  21097  lgsquadlem2  21127  dchrisum0lem1b  21197  pntrlog2bndlem6  21265  pntlemf  21287  ex-ss  21723  shsleji  22860  shsval2i  22877  ssjo  22937  sshhococi  23036  esumsplit  24435  aean  24583  sxbrsigalem2  24624  subfacp1lem2b  24855  subfacp1lem3  24856  subfacp1lem5  24858  kur14lem7  24886  kur14lem9  24888  cvmliftlem10  24969  fprodsplit  25278  fprod2d  25294  dftrpred3g  25491  wfrlem14  25524  wfrlem15  25525  nofulllem4  25614  mbfresfi  26199  refssfne  26311  locfincmp  26321  comppfsc  26324  filnetlem3  26346  prdsbnd  26439  heibor1lem  26455  rrnequiv  26481  ralxpmap  26679  elrfi  26685  mzpcompact2lem  26745  eldioph2  26757  eldioph4b  26809  ttac  27044  pwssplit4  27106  pwslnmlem2  27110  isnumbasgrplem2  27184  fiuneneq  27428  idomsubgmo  27429  compne  27557  bnj931  28995  paddunssN  30444  sspadd1  30451  sspadd2  30452  pclfinN  30536  dochdmj1  32027  dvhdimlem  32081
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator