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

Theorem ssun1 3653
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 383 . . 3  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
2 elun 3631 . . 3  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
31, 2sylibr 212 . 2  |-  ( x  e.  A  ->  x  e.  ( A  u.  B
) )
43ssriv 3493 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 366    e. wcel 1823    u. cun 3459    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-in 3468  df-ss 3475
This theorem is referenced by:  ssun2  3654  ssun3  3655  elun1  3657  inabs  3726  reuun1  3777  un00  3850  snsspr1  4165  snsstp1  4167  snsstp2  4168  uniintsn  4309  sssucid  4944  sofld  5439  fvrn0  5870  ovima0  6427  unexb  6573  dmexg  6704  suppun  6912  dftpos2  6964  tpostpos2  6968  tfrlem11  7049  oaabs2  7286  ralxpmap  7461  domss2  7669  mapunen  7679  ac6sfi  7756  frfi  7757  unfir  7780  domunfican  7785  iunfi  7800  elfiun  7882  dffi3  7883  unwdomg  8002  unxpwdom2  8006  unxpwdom  8007  cantnfp1lem1  8088  cantnfp1lem3  8090  cantnfp1lem1OLD  8114  cantnfp1lem3OLD  8116  tc2  8164  unwf  8219  rankunb  8259  r0weon  8381  infxpenlem  8382  dfac2  8502  cdadom3  8559  cdainflem  8562  infunabs  8578  infcda  8579  infdif  8580  ackbij1lem15  8605  cfsmolem  8641  isfin4-3  8686  fin23lem11  8688  fin1a2lem10  8780  fin1a2lem13  8783  axdc3lem4  8824  axcclem  8828  zornn0g  8876  ttukeylem1  8880  ttukeylem5  8884  ttukeylem7  8886  fingch  8990  fpwwe2lem13  9009  gchac  9048  wunfi  9088  wundm  9095  wunex2  9105  inar1  9142  ressxr  9626  nnssnn0  10794  un0addcl  10825  un0mulcl  10826  hashbclem  12488  hashf1lem1  12491  hashf1lem2  12492  ccatfnOLD  12583  ccatrn  12598  trclublem  12916  relexpdmg  12960  relexpaddg  12971  fsumsplit  13647  fsum2d  13671  fsumabs  13700  fsumrlim  13710  fsumo1  13711  incexclem  13733  fprodsplit  13855  fprod2d  13870  vdwapid1  14580  vdwlem6  14591  ramcl2  14621  isstruct2  14728  srngbase  14847  srngplusg  14848  srngmulr  14849  lmodbase  14856  lmodplusg  14857  lmodsca  14858  ipsbase  14863  ipsaddg  14864  ipsmulr  14865  phlbase  14873  phlplusg  14874  phlsca  14875  odrngbas  14899  odrngplusg  14900  odrngmulr  14901  prdssca  14948  prdsbas  14949  prdsplusg  14950  prdsmulr  14951  prdsvsca  14952  prdsip  14953  prdsle  14954  prdsds  14956  prdstset  14958  imasbas  15004  imasplusg  15009  imasmulr  15010  imassca  15011  imasvsca  15012  imasip  15013  mreexexlem2d  15137  drsdirfi  15769  ipobas  15987  ipotset  15989  acsfiindd  16009  psdmrn  16039  dirdm  16066  gsumzaddlemOLD  17138  gsumzsplit  17146  gsumzsplitOLD  17147  gsumsplit2  17150  gsumzunsnd  17181  gsum2dlem2  17197  gsum2dOLD  17199  dprdfadd  17258  dprdfaddOLD  17265  dmdprdsplit2lem  17292  dmdprdsplit2  17293  dmdprdsplit  17294  dprdsplit  17295  ablfac1eulem  17321  lspun  17831  lspsolv  17987  lsppratlem3  17993  islbs3  17999  lbsextlem2  18003  lbsextlem4  18005  psrbagaddcl  18218  psrbagaddclOLD  18219  psrbas  18228  psrbasOLD  18229  psrplusg  18232  psrmulr  18235  mplsubglem  18291  mplsubglemOLD  18293  mplcoe1  18325  mplcoe5  18329  mplcoe2OLD  18331  cnfldbas  18622  cnfldadd  18623  cnfldmul  18624  cnfldcj  18625  cnfldtset  18626  cnfldle  18627  cnfldds  18628  mdetunilem9  19292  basdif0  19624  ordtbas2  19862  ordtbas  19863  ordtopn1  19865  leordtval2  19883  iocpnfordt  19886  icomnfordt  19887  uncmp  20073  fiuncmp  20074  bwth  20080  locfincmp  20196  comppfsc  20202  1stckgenlem  20223  1stckgen  20224  ptbasin  20247  ptbasfi  20251  dfac14lem  20287  dfac14  20288  ptuncnv  20477  ptunhmeo  20478  ptcmpfi  20483  fbun  20510  trfil2  20557  ufprim  20579  ufileu  20589  filufint  20590  ufildr  20601  fmfnfm  20628  hausflim  20651  fclsfnflim  20697  alexsubALTlem4  20719  tmdgsum  20763  tsmsgsum  20806  tsmsgsumOLD  20809  tsmsresOLD  20814  tsmsres  20815  tsmssplit  20823  tsmsxplem1  20824  ustssco  20886  ustuqtop1  20913  prdsxmetlem  21040  prdsbl  21163  icccmplem2  21497  fsumcn  21543  cnmpt2pc  21597  rrxmetlem  22003  rrxmet  22004  rrxdstprj1  22005  ovolctb2  22072  ovolunnul  22080  ovolfiniun  22081  nulmbl2  22116  finiunmbl  22123  volfiniun  22126  icombl  22143  ioombl  22144  uniiccdif  22156  mbfres2  22221  itg2splitlem  22324  itg2split  22325  itgfsum  22402  itgsplit  22411  itgsplitioo  22413  dvreslem  22482  dvaddbr  22510  dvmulbr  22511  dvmptfsum  22545  lhop  22586  dvcnvrelem2  22588  mdegcl  22638  elplyr  22767  plyrem  22870  xrlimcnp  23499  fsumharmonic  23542  chtdif  23633  lgsdir2lem3  23801  lgsquadlem2  23831  dchrisum0lem1b  23901  pntrlog2bndlem6  23969  pntlemf  23991  ex-ss  25353  shsleji  26489  shsval2i  26506  ssjo  26566  sshhococi  26665  padct  27779  gsumle  28007  gsumvsca1  28011  gsumvsca2  28012  esumsplit  28285  esumpad2  28288  aean  28456  sxbrsigalem2  28497  subfacp1lem2b  28892  subfacp1lem3  28893  subfacp1lem5  28895  kur14lem7  28923  kur14lem9  28925  cvmliftlem10  29006  dftrpred3g  29559  wfrlem14  29599  wfrlem15  29600  nofulllem4  29708  finixpnum  30281  mbfresfi  30304  refssfne  30419  filnetlem3  30441  prdsbnd  30532  heibor1lem  30548  rrnequiv  30574  elrfi  30869  mzpcompact2lem  30926  eldioph2  30937  eldioph4b  30987  ttac  31220  pwssplit4  31277  pwslnmlem2  31281  isnumbasgrplem2  31297  algbase  31371  algaddg  31372  algmulr  31373  fiuneneq  31398  idomsubgmo  31399  compne  31593  mccllem  31847  cncfiooicclem1  31938  dvmptfprod  31984  dvnprodlem1  31985  iblsplit  32007  fourierdlem54  32185  fourierdlem102  32233  fourierdlem103  32234  fourierdlem104  32235  fourierdlem114  32245  gsumsplit2f  33227  bnj931  34249  bj-unrab  34914  bj-snglsstag  34959  bj-2upln0  35001  bj-ccssccbar  35039  paddunssN  35948  sspadd1  35955  sspadd2  35956  pclfinN  36040  dochdmj1  37533  dvhdimlem  37587  dfrcl2  38214  relexpaddss  38226  relexp0a  38244  trclimalb2  38260
  Copyright terms: Public domain W3C validator