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

Theorem ssun1 4134
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 864 . . 3 (𝑥𝐴 → (𝑥𝐴𝑥𝐵))
2 elun 4111 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
31, 2sylibr 237 . 2 (𝑥𝐴𝑥 ∈ (𝐴𝐵))
43ssriv 3957 1 𝐴 ⊆ (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 844  wcel 2115  cun 3917  wss 3919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924  df-in 3926  df-ss 3936
This theorem is referenced by:  ssun2  4135  ssun3  4136  elun1  4138  difsssymdif  4214  inabs  4217  reuun1  4270  un00  4377  pwunss  4542  pwundif  4548  snsspr1  4731  snsstp1  4733  snsstp2  4734  uniintsn  4899  sofld  6031  sssucid  6255  fvrn0  6689  ovima0  7321  unexb  7465  dmexg  7608  suppun  7846  dftpos2  7905  tpostpos2  7909  wfrlem14  7964  wfrlem15  7965  tfrlem11  8020  oaabs2  8268  ralxpmap  8456  domss2  8673  mapunen  8683  ac6sfi  8759  frfi  8760  unfir  8783  domunfican  8788  iunfi  8809  elfiun  8891  dffi3  8892  unwdomg  9045  unxpwdom2  9049  unxpwdom  9050  cantnfp1lem1  9138  cantnfp1lem3  9140  tc2  9181  unwf  9236  rankunb  9276  r0weon  9436  infxpenlem  9437  dfac2b  9554  djudoml  9608  cdainflem  9611  infunabs  9627  infdju  9628  infdif  9629  ackbij1lem15  9654  cfsmolem  9690  isfin4p1  9735  fin23lem11  9737  fin1a2lem10  9829  fin1a2lem13  9832  axdc3lem4  9873  axcclem  9877  zornn0g  9925  ttukeylem1  9929  ttukeylem5  9933  ttukeylem7  9935  fingch  10043  fpwwe2lem13  10062  gchac  10101  wunfi  10141  wundm  10148  wunex2  10158  inar1  10195  ressxr  10683  nnssnn0  11897  un0addcl  11927  un0mulcl  11928  nn0ssxnn0  11967  hashbclem  13815  hashf1lem1  13818  hashf1lem2  13819  ccatrn  13943  trclublem  14355  relexpdmg  14401  relexpaddg  14412  fsumsplit  15097  fsum2d  15126  fsumabs  15156  fsumrlim  15166  fsumo1  15167  incexclem  15191  fprodsplit  15320  fprod2d  15335  lcmfunsnlem1  15979  coprmprod  16003  vdwapid1  16309  vdwlem6  16320  ramcl2  16350  isstruct2  16493  srngbase  16628  srngplusg  16629  srngmulr  16630  lmodbase  16637  lmodplusg  16638  lmodsca  16639  ipsbase  16644  ipsaddg  16645  ipsmulr  16646  phlbase  16654  phlplusg  16655  phlsca  16656  odrngbas  16680  odrngplusg  16681  odrngmulr  16682  prdssca  16729  prdsbas  16730  prdsplusg  16731  prdsmulr  16732  prdsvsca  16733  prdsip  16734  prdsle  16735  prdsds  16737  prdstset  16739  imasbas  16785  imasplusg  16790  imasmulr  16791  imassca  16792  imasvsca  16793  imasip  16794  mreexexlem2d  16916  drsdirfi  17548  ipobas  17765  ipotset  17767  acsfiindd  17787  psdmrn  17817  dirdm  17844  grpinvfval  18142  mulgfval  18226  gsumzsplit  19047  gsumsplit2  19049  gsumzunsnd  19076  gsum2dlem2  19091  dprdfadd  19142  dmdprdsplit2lem  19167  dmdprdsplit2  19168  dmdprdsplit  19169  dprdsplit  19170  ablfac1eulem  19194  lspun  19759  lspsolv  19915  lsppratlem3  19921  islbs3  19927  lbsextlem2  19931  lbsextlem4  19933  psrbagaddcl  20150  psrbas  20158  psrplusg  20161  psrmulr  20164  mplsubglem  20214  mplcoe1  20246  mplcoe5  20249  cnfldbas  20549  cnfldadd  20550  cnfldmul  20551  cnfldcj  20552  cnfldtset  20553  cnfldle  20554  cnfldds  20555  mdetunilem9  21229  basdif0  21561  ordtbas2  21799  ordtbas  21800  ordtopn1  21802  leordtval2  21820  iocpnfordt  21823  icomnfordt  21824  uncmp  22011  fiuncmp  22012  bwth  22018  locfincmp  22134  comppfsc  22140  1stckgenlem  22161  1stckgen  22162  ptbasin  22185  ptbasfi  22189  dfac14lem  22225  dfac14  22226  ptuncnv  22415  ptunhmeo  22416  ptcmpfi  22421  fbun  22448  trfil2  22495  ufprim  22517  ufileu  22527  filufint  22528  ufildr  22539  fmfnfm  22566  hausflim  22589  fclsfnflim  22635  alexsubALTlem4  22658  tmdgsum  22703  tsmsgsum  22747  tsmsres  22752  tsmssplit  22760  tsmsxplem1  22761  ustssco  22823  ustuqtop1  22850  prdsxmetlem  22978  prdsbl  23101  icccmplem2  23431  fsumcn  23478  cnmpopc  23536  rrxmetlem  24014  rrxmet  24015  rrxdstprj1  24016  ovolctb2  24099  ovolunnul  24107  ovolfiniun  24108  nulmbl2  24143  finiunmbl  24151  volfiniun  24154  icombl  24171  ioombl  24172  uniiccdif  24185  mbfres2  24252  itg2splitlem  24355  itg2split  24356  itgfsum  24433  itgsplit  24442  itgsplitioo  24444  dvreslem  24515  dvaddbr  24544  dvmulbr  24545  dvmptfsum  24581  lhop  24622  dvcnvrelem2  24624  mdegcl  24673  elplyr  24801  plyrem  24904  xrlimcnp  25557  fsumharmonic  25600  chtdif  25746  lgsdir2lem3  25914  lgsquadlem2  25968  dchrisum0lem1b  26102  pntrlog2bndlem6  26170  pntlemf  26192  ex-ss  28215  shsleji  29156  shsval2i  29173  ssjo  29233  sshhococi  29332  padct  30466  gsumle  30757  symgcom  30759  cycpmco2lem5  30804  cycpmco2lem6  30805  cycpmco2lem7  30806  cycpmco2  30807  gsumvsca1  30886  gsumvsca2  30887  mxidlprm  31018  idlsrgbas  31027  idlsrgplusg  31028  idlsrgmulr  31030  esumsplit  31369  esumpad2  31372  aean  31560  sxbrsigalem2  31601  bnj931  32099  subfacp1lem2b  32485  subfacp1lem3  32486  subfacp1lem5  32488  kur14lem7  32516  kur14lem9  32518  cvmliftlem10  32598  satfsschain  32668  fmlasssuc  32693  dftrpred3g  33129  frrlem12  33191  frrlem13  33192  scutun12  33328  refssfne  33763  filnetlem3  33785  bj-unrab  34312  bj-snglsstag  34361  bj-2upln0  34403  bj-ccssccbar  34577  rdgssun  34740  finixpnum  34987  matunitlindflem1  34998  mbfresfi  35048  prdsbnd  35176  heibor1lem  35192  rrnequiv  35218  paddunssN  37049  sspadd1  37056  sspadd2  37057  pclfinN  37141  dochdmj1  38631  dvhdimlem  38685  elrfi  39551  mzpcompact2lem  39608  eldioph2  39619  eldioph4b  39668  ttac  39893  pwssplit4  39949  pwslnmlem2  39953  isnumbasgrplem2  39964  algbase  40038  algaddg  40039  algmulr  40040  fiuneneq  40057  idomsubgmo  40058  rclexi  40231  rtrclex  40233  trclubgNEW  40234  trclexi  40236  rtrclexi  40237  cnvrcl0  40241  cnvtrcl0  40242  dfrtrcl5  40245  trrelsuperrel2dg  40288  dfrcl2  40291  relexp0a  40333  relexpaddss  40335  trclimalb2  40343  frege83d  40365  frege131d  40381  dssmapnvod  40638  clsk3nimkb  40662  isotone1  40670  grumnudlem  40913  infxrpnf  42010  mccllem  42165  cncfiooicclem1  42461  dvmptfprod  42513  dvnprodlem1  42514  iblsplit  42534  fourierdlem54  42728  fourierdlem102  42776  fourierdlem103  42777  fourierdlem104  42778  fourierdlem114  42788  sge0resplit  42971  sge0split  42974  sge0splitmpt  42976  sge0xaddlem1  42998  isomenndlem  43095  hoiprodp1  43153  hoidmvlelem1  43160  hoidmvlelem2  43161  hoidmvlelem3  43162  hoidmvlelem4  43163  gsumsplit2f  44366  setrec1lem4  45146  elpglem2  45167
  Copyright terms: Public domain W3C validator