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

Theorem ssun1 3478
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 3456 . . 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 3320 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    \/ wo 358    e. wcel 1721    u. cun 3286    C_ wss 3288
This theorem is referenced by:  ssun2  3479  ssun3  3480  elun1  3482  inabs  3540  reuun1  3591  un00  3631  snsspr1  3915  snsstp1  3917  snsstp2  3918  uniintsn  4055  sssucid  4626  unexb  4676  dmexg  5097  sofld  5285  fvrn0  5720  dftpos2  6463  tpostpos2  6467  riotassuni  6555  tfrlem11  6616  oaabs2  6855  domss2  7233  mapunen  7243  ac6sfi  7318  frfi  7319  unfir  7342  domunfican  7346  iunfi  7361  elfiun  7401  dffi3  7402  unwdomg  7516  unxpwdom2  7520  unxpwdom  7521  cantnfp1lem1  7598  cantnfp1lem3  7600  tc2  7645  unwf  7700  rankunb  7740  r0weon  7858  infxpenlem  7859  dfac2  7975  cdadom3  8032  cdainflem  8035  infunabs  8051  infcda  8052  infdif  8053  ackbij1lem15  8078  cfsmolem  8114  isfin4-3  8159  fin23lem11  8161  fin1a2lem10  8253  fin1a2lem13  8256  axdc3lem4  8297  axcclem  8301  zornn0g  8349  ttukeylem1  8353  ttukeylem5  8357  ttukeylem7  8359  fingch  8462  fpwwe2lem13  8481  gchac  8512  wunfi  8560  wundm  8567  wunex2  8577  inar1  8614  ressxr  9093  nnssnn0  10188  un0addcl  10217  un0mulcl  10218  hashbclem  11664  hashf1lem1  11667  hashf1lem2  11668  ccatfn  11704  fsumsplit  12496  fsum2d  12518  fsumabs  12543  fsumrlim  12553  fsumo1  12554  incexclem  12579  vdwapid1  13306  vdwlem6  13317  ramcl2  13347  isstruct2  13441  srngbase  13548  srngplusg  13549  srngmulr  13550  lmodbase  13557  lmodplusg  13558  lmodsca  13559  algbase  13562  algaddg  13563  algmulr  13564  phlbase  13572  phlplusg  13573  phlsca  13574  odrngbas  13598  odrngplusg  13599  odrngmulr  13600  prdssca  13642  prdsbas  13643  prdsplusg  13644  prdsmulr  13645  prdsvsca  13646  prdsle  13647  prdsds  13649  prdstset  13651  imasbas  13701  imasplusg  13706  imasmulr  13707  imassca  13708  imasvsca  13709  mreexexlem2d  13833  drsdirfi  14358  ipobas  14544  ipotset  14546  acsfiindd  14566  psdmrn  14602  dirdm  14642  gsumzaddlem  15489  gsumzsplit  15492  gsumsplit2  15494  gsum2d  15509  dprdfadd  15541  dmdprdsplit2lem  15566  dmdprdsplit2  15567  dmdprdsplit  15568  dprdsplit  15569  ablfac1eulem  15593  lspun  16026  lspsolv  16178  lsppratlem3  16184  islbs3  16190  lbsextlem2  16194  lbsextlem4  16196  psrbagaddcl  16398  psrbas  16406  psrplusg  16408  psrmulr  16411  mplsubglem  16461  mplcoe1  16491  mplcoe2  16493  cnfldbas  16670  cnfldadd  16671  cnfldmul  16672  cnfldcj  16673  cnfldtset  16674  cnfldle  16675  cnfldds  16676  basdif0  16981  tgdif0  17020  ordtbas2  17217  ordtbas  17218  ordtopn1  17220  leordtval2  17238  iocpnfordt  17241  icomnfordt  17242  uncmp  17428  fiuncmp  17429  1stckgenlem  17546  1stckgen  17547  ptbasin  17570  ptbasfi  17574  dfac14lem  17610  dfac14  17611  ptuncnv  17800  ptunhmeo  17801  ptcmpfi  17806  fbun  17833  trfil2  17880  ufprim  17902  ufileu  17912  filufint  17913  ufildr  17924  fmfnfm  17951  hausflim  17974  fclsfnflim  18020  alexsubALTlem4  18042  tmdgsum  18086  tsmsgsum  18129  tsmsres  18134  tsmssplit  18142  tsmsxplem1  18143  ustssco  18205  ustuqtop1  18232  prdsxmetlem  18359  prdsbl  18482  icccmplem2  18815  fsumcn  18861  cnmpt2pc  18914  iccpnfcnv  18930  ovolctb2  19349  ovolunnul  19357  ovolfiniun  19358  nulmbl2  19392  finiunmbl  19399  volfiniun  19402  icombl  19419  ioombl  19420  uniiccdif  19431  mbfres2  19498  itg2splitlem  19601  itg2split  19602  itgfsum  19679  itgsplit  19688  itgsplitioo  19690  dvreslem  19757  dvaddbr  19785  dvmulbr  19786  dvmptfsum  19820  lhop  19861  dvcnvrelem2  19863  mdegcl  19953  elplyr  20081  plyrem  20183  xrlimcnp  20768  fsumharmonic  20811  chtdif  20902  lgsdir2lem3  21070  lgsquadlem2  21100  dchrisum0lem1b  21170  pntrlog2bndlem6  21238  pntlemf  21260  ex-ss  21696  shsleji  22833  shsval2i  22850  ssjo  22910  sshhococi  23009  esumsplit  24408  aean  24556  sxbrsigalem2  24597  subfacp1lem2b  24828  subfacp1lem3  24829  subfacp1lem5  24831  kur14lem7  24859  kur14lem9  24861  cvmliftlem10  24942  fprodsplit  25250  fprod2d  25266  dftrpred3g  25458  wfrlem14  25491  wfrlem15  25492  nofulllem4  25581  mbfresfi  26160  refssfne  26272  locfincmp  26282  comppfsc  26285  filnetlem3  26307  prdsbnd  26400  heibor1lem  26416  rrnequiv  26442  ralxpmap  26640  elrfi  26646  mzpcompact2lem  26706  eldioph2  26718  eldioph4b  26770  ttac  27005  pwssplit4  27067  pwslnmlem2  27071  isnumbasgrplem2  27145  fiuneneq  27389  idomsubgmo  27390  compne  27518  bnj931  28859  paddunssN  30302  sspadd1  30309  sspadd2  30310  pclfinN  30394  dochdmj1  31885  dvhdimlem  31939
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 2393
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 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-un 3293  df-in 3295  df-ss 3302
  Copyright terms: Public domain W3C validator