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

Theorem ssun1 3540
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 385 . . 3  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
2 elun 3518 . . 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 3381 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    e. wcel 1756    u. cun 3347    C_ wss 3349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-un 3354  df-in 3356  df-ss 3363
This theorem is referenced by:  ssun2  3541  ssun3  3542  elun1  3544  inabs  3602  reuun1  3653  un00  3735  snsspr1  4043  snsstp1  4045  snsstp2  4046  uniintsn  4186  sssucid  4817  sofld  5307  fvrn0  5733  ovima0  6263  unexb  6401  dmexg  6530  suppun  6730  dftpos2  6783  tpostpos2  6787  tfrlem11  6868  oaabs2  7105  ralxpmap  7283  domss2  7491  mapunen  7501  ac6sfi  7577  frfi  7578  unfir  7601  domunfican  7605  iunfi  7620  elfiun  7701  dffi3  7702  unwdomg  7820  unxpwdom2  7824  unxpwdom  7825  cantnfp1lem1  7907  cantnfp1lem3  7909  cantnfp1lem1OLD  7933  cantnfp1lem3OLD  7935  tc2  7983  unwf  8038  rankunb  8078  r0weon  8200  infxpenlem  8201  dfac2  8321  cdadom3  8378  cdainflem  8381  infunabs  8397  infcda  8398  infdif  8399  ackbij1lem15  8424  cfsmolem  8460  isfin4-3  8505  fin23lem11  8507  fin1a2lem10  8599  fin1a2lem13  8602  axdc3lem4  8643  axcclem  8647  zornn0g  8695  ttukeylem1  8699  ttukeylem5  8703  ttukeylem7  8705  fingch  8811  fpwwe2lem13  8830  gchac  8869  wunfi  8909  wundm  8916  wunex2  8926  inar1  8963  ressxr  9448  nnssnn0  10603  un0addcl  10634  un0mulcl  10635  hashbclem  12226  hashf1lem1  12229  hashf1lem2  12230  ccatfn  12293  fsumsplit  13237  fsum2d  13259  fsumabs  13285  fsumrlim  13295  fsumo1  13296  incexclem  13320  vdwapid1  14057  vdwlem6  14068  ramcl2  14098  isstruct2  14204  srngbase  14315  srngplusg  14316  srngmulr  14317  lmodbase  14324  lmodplusg  14325  lmodsca  14326  ipsbase  14331  ipsaddg  14332  ipsmulr  14333  phlbase  14341  phlplusg  14342  phlsca  14343  odrngbas  14367  odrngplusg  14368  odrngmulr  14369  prdssca  14415  prdsbas  14416  prdsplusg  14417  prdsmulr  14418  prdsvsca  14419  prdsip  14420  prdsle  14421  prdsds  14423  prdstset  14425  imasbas  14471  imasplusg  14476  imasmulr  14477  imassca  14478  imasvsca  14479  imasip  14480  mreexexlem2d  14604  drsdirfi  15129  ipobas  15346  ipotset  15348  acsfiindd  15368  psdmrn  15398  dirdm  15425  gsumzaddlemOLD  16431  gsumzsplit  16439  gsumzsplitOLD  16440  gsumsplit2  16443  gsumsplit2OLD  16444  gsumzunsnd  16473  gsum2dlem2  16484  gsum2dOLD  16486  dprdfadd  16532  dprdfaddOLD  16539  dmdprdsplit2lem  16566  dmdprdsplit2  16567  dmdprdsplit  16568  dprdsplit  16569  ablfac1eulem  16595  lspun  17090  lspsolv  17246  lsppratlem3  17252  islbs3  17258  lbsextlem2  17262  lbsextlem4  17264  psrbagaddcl  17460  psrbagaddclOLD  17461  psrbas  17470  psrbasOLD  17471  psrplusg  17474  psrmulr  17477  mplsubglem  17532  mplsubglemOLD  17534  mplcoe1  17566  mplcoe5  17570  mplcoe2OLD  17572  cnfldbas  17844  cnfldadd  17845  cnfldmul  17846  cnfldcj  17847  cnfldtset  17848  cnfldle  17849  cnfldds  17850  mdetunilem9  18448  basdif0  18580  tgdif0  18619  ordtbas2  18817  ordtbas  18818  ordtopn1  18820  leordtval2  18838  iocpnfordt  18841  icomnfordt  18842  uncmp  19028  fiuncmp  19029  bwth  19035  1stckgenlem  19148  1stckgen  19149  ptbasin  19172  ptbasfi  19176  dfac14lem  19212  dfac14  19213  ptuncnv  19402  ptunhmeo  19403  ptcmpfi  19408  fbun  19435  trfil2  19482  ufprim  19504  ufileu  19514  filufint  19515  ufildr  19526  fmfnfm  19553  hausflim  19576  fclsfnflim  19622  alexsubALTlem4  19644  tmdgsum  19688  tsmsgsum  19731  tsmsgsumOLD  19734  tsmsresOLD  19739  tsmsres  19740  tsmssplit  19748  tsmsxplem1  19749  ustssco  19811  ustuqtop1  19838  prdsxmetlem  19965  prdsbl  20088  icccmplem2  20422  fsumcn  20468  cnmpt2pc  20522  iccpnfcnv  20538  rrxmetlem  20928  rrxmet  20929  rrxdstprj1  20930  ovolctb2  20997  ovolunnul  21005  ovolfiniun  21006  nulmbl2  21040  finiunmbl  21047  volfiniun  21050  icombl  21067  ioombl  21068  uniiccdif  21080  mbfres2  21145  itg2splitlem  21248  itg2split  21249  itgfsum  21326  itgsplit  21335  itgsplitioo  21337  dvreslem  21406  dvaddbr  21434  dvmulbr  21435  dvmptfsum  21469  lhop  21510  dvcnvrelem2  21512  mdegcl  21562  elplyr  21691  plyrem  21793  xrlimcnp  22384  fsumharmonic  22427  chtdif  22518  lgsdir2lem3  22686  lgsquadlem2  22716  dchrisum0lem1b  22786  pntrlog2bndlem6  22854  pntlemf  22876  ex-ss  23656  shsleji  24795  shsval2i  24812  ssjo  24872  sshhococi  24971  gsumle  26268  gsummptun  26270  gsumvsca1  26273  gsumvsca2  26274  esumsplit  26528  aean  26682  sxbrsigalem2  26723  subfacp1lem2b  27091  subfacp1lem3  27092  subfacp1lem5  27094  kur14lem7  27122  kur14lem9  27124  cvmliftlem10  27205  fprodsplit  27498  fprod2d  27514  dftrpred3g  27719  wfrlem14  27759  wfrlem15  27760  nofulllem4  27868  finixpnum  28440  mbfresfi  28464  refssfne  28592  locfincmp  28602  comppfsc  28605  filnetlem3  28627  prdsbnd  28718  heibor1lem  28734  rrnequiv  28760  elrfi  29056  mzpcompact2lem  29114  eldioph2  29126  eldioph4b  29176  ttac  29411  pwssplit4  29468  pwslnmlem2  29472  isnumbasgrplem2  29486  algbase  29561  algaddg  29562  algmulr  29563  fiuneneq  29588  idomsubgmo  29589  compne  29722  gsumsplit2f  30793  bnj931  31860  bj-unrab  32525  bj-snglsstag  32570  bj-2upln0  32612  bj-ccssccbar  32636  paddunssN  33548  sspadd1  33555  sspadd2  33556  pclfinN  33640  dochdmj1  35131  dvhdimlem  35185
  Copyright terms: Public domain W3C validator