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

Theorem ssun1 3738
Description: Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ssun1 𝐴 ⊆ (𝐴𝐵)

Proof of Theorem ssun1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 orc 399 . . 3 (𝑥𝐴 → (𝑥𝐴𝑥𝐵))
2 elun 3715 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
31, 2sylibr 223 . 2 (𝑥𝐴𝑥 ∈ (𝐴𝐵))
43ssriv 3572 1 𝐴 ⊆ (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 382  wcel 1977  cun 3538  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554
This theorem is referenced by:  ssun2  3739  ssun3  3740  elun1  3742  inabs  3817  reuun1  3868  un00  3963  snsspr1  4285  snsstp1  4287  snsstp2  4288  uniintsn  4449  sofld  5500  sssucid  5719  fvrn0  6126  ovima0  6711  unexb  6856  dmexg  6989  suppun  7202  dftpos2  7256  tpostpos2  7260  wfrlem14  7315  wfrlem15  7316  tfrlem11  7371  oaabs2  7612  ralxpmap  7793  domss2  8004  mapunen  8014  ac6sfi  8089  frfi  8090  unfir  8113  domunfican  8118  iunfi  8137  elfiun  8219  dffi3  8220  unwdomg  8372  unxpwdom2  8376  unxpwdom  8377  cantnfp1lem1  8458  cantnfp1lem3  8460  tc2  8501  unwf  8556  rankunb  8596  r0weon  8718  infxpenlem  8719  dfac2  8836  cdadom3  8893  cdainflem  8896  infunabs  8912  infcda  8913  infdif  8914  ackbij1lem15  8939  cfsmolem  8975  isfin4-3  9020  fin23lem11  9022  fin1a2lem10  9114  fin1a2lem13  9117  axdc3lem4  9158  axcclem  9162  zornn0g  9210  ttukeylem1  9214  ttukeylem5  9218  ttukeylem7  9220  fingch  9324  fpwwe2lem13  9343  gchac  9382  wunfi  9422  wundm  9429  wunex2  9439  inar1  9476  ressxr  9962  nnssnn0  11172  un0addcl  11203  un0mulcl  11204  nn0ssxnn0  11243  hashbclem  13093  hashf1lem1  13096  hashf1lem2  13097  ccatrn  13225  trclublem  13582  relexpdmg  13630  relexpaddg  13641  fsumsplit  14318  fsum2d  14344  fsumabs  14374  fsumrlim  14384  fsumo1  14385  incexclem  14407  fprodsplit  14535  fprod2d  14550  lcmfunsnlem1  15188  coprmprod  15213  vdwapid1  15517  vdwlem6  15528  ramcl2  15558  isstruct2  15704  srngbase  15832  srngplusg  15833  srngmulr  15834  lmodbase  15841  lmodplusg  15842  lmodsca  15843  ipsbase  15848  ipsaddg  15849  ipsmulr  15850  phlbase  15858  phlplusg  15859  phlsca  15860  odrngbas  15890  odrngplusg  15891  odrngmulr  15892  prdssca  15939  prdsbas  15940  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  prdsip  15944  prdsle  15945  prdsds  15947  prdstset  15949  imasbas  15995  imasplusg  16000  imasmulr  16001  imassca  16002  imasvsca  16003  imasip  16004  mreexexlem2d  16128  drsdirfi  16761  ipobas  16978  ipotset  16980  acsfiindd  17000  psdmrn  17030  dirdm  17057  gsumzsplit  18150  gsumsplit2  18152  gsumzunsnd  18178  gsum2dlem2  18193  dprdfadd  18242  dmdprdsplit2lem  18267  dmdprdsplit2  18268  dmdprdsplit  18269  dprdsplit  18270  ablfac1eulem  18294  lspun  18808  lspsolv  18964  lsppratlem3  18970  islbs3  18976  lbsextlem2  18980  lbsextlem4  18982  psrbagaddcl  19191  psrbas  19199  psrplusg  19202  psrmulr  19205  mplsubglem  19255  mplcoe1  19286  mplcoe5  19289  cnfldbas  19571  cnfldadd  19572  cnfldmul  19573  cnfldcj  19574  cnfldtset  19575  cnfldle  19576  cnfldds  19577  mdetunilem9  20245  basdif0  20568  ordtbas2  20805  ordtbas  20806  ordtopn1  20808  leordtval2  20826  iocpnfordt  20829  icomnfordt  20830  uncmp  21016  fiuncmp  21017  bwth  21023  locfincmp  21139  comppfsc  21145  1stckgenlem  21166  1stckgen  21167  ptbasin  21190  ptbasfi  21194  dfac14lem  21230  dfac14  21231  ptuncnv  21420  ptunhmeo  21421  ptcmpfi  21426  fbun  21454  trfil2  21501  ufprim  21523  ufileu  21533  filufint  21534  ufildr  21545  fmfnfm  21572  hausflim  21595  fclsfnflim  21641  alexsubALTlem4  21664  tmdgsum  21709  tsmsgsum  21752  tsmsres  21757  tsmssplit  21765  tsmsxplem1  21766  ustssco  21828  ustuqtop1  21855  prdsxmetlem  21983  prdsbl  22106  icccmplem2  22434  fsumcn  22481  cnmpt2pc  22535  rrxmetlem  22998  rrxmet  22999  rrxdstprj1  23000  ovolctb2  23067  ovolunnul  23075  ovolfiniun  23076  nulmbl2  23111  finiunmbl  23119  volfiniun  23122  icombl  23139  ioombl  23140  uniiccdif  23152  mbfres2  23218  itg2splitlem  23321  itg2split  23322  itgfsum  23399  itgsplit  23408  itgsplitioo  23410  dvreslem  23479  dvaddbr  23507  dvmulbr  23508  dvmptfsum  23542  lhop  23583  dvcnvrelem2  23585  mdegcl  23633  elplyr  23761  plyrem  23864  xrlimcnp  24495  fsumharmonic  24538  chtdif  24684  lgsdir2lem3  24852  lgsquadlem2  24906  dchrisum0lem1b  25004  pntrlog2bndlem6  25072  pntlemf  25094  ex-ss  26676  shsleji  27613  shsval2i  27630  ssjo  27690  sshhococi  27789  padct  28885  gsumle  29110  gsumvsca1  29113  gsumvsca2  29114  esumsplit  29442  esumpad2  29445  aean  29634  sxbrsigalem2  29675  bnj931  30095  subfacp1lem2b  30417  subfacp1lem3  30418  subfacp1lem5  30420  kur14lem7  30448  kur14lem9  30450  cvmliftlem10  30530  dftrpred3g  30977  nofulllem4  31104  refssfne  31523  filnetlem3  31545  bj-unrab  32114  bj-snglsstag  32162  bj-2upln0  32204  bj-ccssccbar  32281  finixpnum  32564  matunitlindflem1  32575  mbfresfi  32626  prdsbnd  32762  heibor1lem  32778  rrnequiv  32804  paddunssN  34112  sspadd1  34119  sspadd2  34120  pclfinN  34204  dochdmj1  35697  dvhdimlem  35751  elrfi  36275  mzpcompact2lem  36332  eldioph2  36343  eldioph4b  36393  ttac  36621  pwssplit4  36677  pwslnmlem2  36681  isnumbasgrplem2  36693  algbase  36767  algaddg  36768  algmulr  36769  fiuneneq  36794  idomsubgmo  36795  rclexi  36941  rtrclex  36943  trclubgNEW  36944  trclexi  36946  rtrclexi  36947  cnvrcl0  36951  cnvtrcl0  36952  dfrtrcl5  36955  trrelsuperrel2dg  36982  dfrcl2  36985  relexp0a  37027  relexpaddss  37029  trclimalb2  37037  frege83d  37059  frege131d  37075  dssmapnvod  37334  clsk3nimkb  37358  isotone1  37366  compne  37665  mccllem  38664  cncfiooicclem1  38779  dvmptfprod  38835  dvnprodlem1  38836  iblsplit  38858  fourierdlem54  39053  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem114  39113  sge0resplit  39299  sge0split  39302  sge0splitmpt  39304  sge0xaddlem1  39326  isomenndlem  39420  hoiprodp1  39478  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  gsumsplit2f  41936  setrec1lem4  42236  elpglem2  42254
  Copyright terms: Public domain W3C validator