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

Theorem ssun1 3470
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 3448 . . 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 3312 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    \/ wo 358    e. wcel 1721    u. cun 3278    C_ wss 3280
This theorem is referenced by:  ssun2  3471  ssun3  3472  elun1  3474  inabs  3532  reuun1  3583  un00  3623  snsspr1  3907  snsstp1  3909  snsstp2  3910  uniintsn  4047  sssucid  4618  unexb  4668  dmexg  5089  sofld  5277  fvrn0  5712  dftpos2  6455  tpostpos2  6459  riotassuni  6547  tfrlem11  6608  oaabs2  6847  domss2  7225  mapunen  7235  ac6sfi  7310  frfi  7311  unfir  7334  domunfican  7338  iunfi  7353  elfiun  7393  dffi3  7394  unwdomg  7508  unxpwdom2  7512  unxpwdom  7513  cantnfp1lem1  7590  cantnfp1lem3  7592  tc2  7637  unwf  7692  rankunb  7732  r0weon  7850  infxpenlem  7851  dfac2  7967  cdadom3  8024  cdainflem  8027  infunabs  8043  infcda  8044  infdif  8045  ackbij1lem15  8070  cfsmolem  8106  isfin4-3  8151  fin23lem11  8153  fin1a2lem10  8245  fin1a2lem13  8248  axdc3lem4  8289  axcclem  8293  zornn0g  8341  ttukeylem1  8345  ttukeylem5  8349  ttukeylem7  8351  fingch  8454  fpwwe2lem13  8473  gchac  8504  wunfi  8552  wundm  8559  wunex2  8569  inar1  8606  ressxr  9085  nnssnn0  10180  un0addcl  10209  un0mulcl  10210  hashbclem  11656  hashf1lem1  11659  hashf1lem2  11660  ccatfn  11696  fsumsplit  12488  fsum2d  12510  fsumabs  12535  fsumrlim  12545  fsumo1  12546  incexclem  12571  vdwapid1  13298  vdwlem6  13309  ramcl2  13339  isstruct2  13433  srngbase  13540  srngplusg  13541  srngmulr  13542  lmodbase  13549  lmodplusg  13550  lmodsca  13551  algbase  13554  algaddg  13555  algmulr  13556  phlbase  13564  phlplusg  13565  phlsca  13566  odrngbas  13590  odrngplusg  13591  odrngmulr  13592  prdssca  13634  prdsbas  13635  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  prdsle  13639  prdsds  13641  prdstset  13643  imasbas  13693  imasplusg  13698  imasmulr  13699  imassca  13700  imasvsca  13701  mreexexlem2d  13825  drsdirfi  14350  ipobas  14536  ipotset  14538  acsfiindd  14558  psdmrn  14594  dirdm  14634  gsumzaddlem  15481  gsumzsplit  15484  gsumsplit2  15486  gsum2d  15501  dprdfadd  15533  dmdprdsplit2lem  15558  dmdprdsplit2  15559  dmdprdsplit  15560  dprdsplit  15561  ablfac1eulem  15585  lspun  16018  lspsolv  16170  lsppratlem3  16176  islbs3  16182  lbsextlem2  16186  lbsextlem4  16188  psrbagaddcl  16390  psrbas  16398  psrplusg  16400  psrmulr  16403  mplsubglem  16453  mplcoe1  16483  mplcoe2  16485  cnfldbas  16662  cnfldadd  16663  cnfldmul  16664  cnfldcj  16665  cnfldtset  16666  cnfldle  16667  cnfldds  16668  basdif0  16973  tgdif0  17012  ordtbas2  17209  ordtbas  17210  ordtopn1  17212  leordtval2  17230  iocpnfordt  17233  icomnfordt  17234  uncmp  17420  fiuncmp  17421  1stckgenlem  17538  1stckgen  17539  ptbasin  17562  ptbasfi  17566  dfac14lem  17602  dfac14  17603  ptuncnv  17792  ptunhmeo  17793  ptcmpfi  17798  fbun  17825  trfil2  17872  ufprim  17894  ufileu  17904  filufint  17905  ufildr  17916  fmfnfm  17943  hausflim  17966  fclsfnflim  18012  alexsubALTlem4  18034  tmdgsum  18078  tsmsgsum  18121  tsmsres  18126  tsmssplit  18134  tsmsxplem1  18135  ustssco  18197  ustuqtop1  18224  prdsxmetlem  18351  prdsbl  18474  icccmplem2  18807  fsumcn  18853  cnmpt2pc  18906  iccpnfcnv  18922  ovolctb2  19341  ovolunnul  19349  ovolfiniun  19350  nulmbl2  19384  finiunmbl  19391  volfiniun  19394  icombl  19411  ioombl  19412  uniiccdif  19423  mbfres2  19490  itg2splitlem  19593  itg2split  19594  itgfsum  19671  itgsplit  19680  itgsplitioo  19682  dvreslem  19749  dvaddbr  19777  dvmulbr  19778  dvmptfsum  19812  lhop  19853  dvcnvrelem2  19855  mdegcl  19945  elplyr  20073  plyrem  20175  xrlimcnp  20760  fsumharmonic  20803  chtdif  20894  lgsdir2lem3  21062  lgsquadlem2  21092  dchrisum0lem1b  21162  pntrlog2bndlem6  21230  pntlemf  21252  ex-ss  21688  shsleji  22825  shsval2i  22842  ssjo  22902  sshhococi  23001  esumsplit  24400  aean  24548  sxbrsigalem2  24589  subfacp1lem2b  24820  subfacp1lem3  24821  subfacp1lem5  24823  kur14lem7  24851  kur14lem9  24853  cvmliftlem10  24934  fprodsplit  25242  fprod2d  25258  dftrpred3g  25450  wfrlem14  25483  wfrlem15  25484  nofulllem4  25573  mbfresfi  26152  refssfne  26264  locfincmp  26274  comppfsc  26277  filnetlem3  26299  prdsbnd  26392  heibor1lem  26408  rrnequiv  26434  ralxpmap  26632  elrfi  26638  mzpcompact2lem  26698  eldioph2  26710  eldioph4b  26762  ttac  26997  pwssplit4  27059  pwslnmlem2  27063  isnumbasgrplem2  27137  fiuneneq  27381  idomsubgmo  27382  compne  27510  bnj931  28847  paddunssN  30290  sspadd1  30297  sspadd2  30298  pclfinN  30382  dochdmj1  31873  dvhdimlem  31927
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator