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

Theorem ssun1 3760
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 400 . . 3 (𝑥𝐴 → (𝑥𝐴𝑥𝐵))
2 elun 3737 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
31, 2sylibr 224 . 2 (𝑥𝐴𝑥 ∈ (𝐴𝐵))
43ssriv 3592 1 𝐴 ⊆ (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 383  wcel 1987  cun 3558  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-un 3565  df-in 3567  df-ss 3574
This theorem is referenced by:  ssun2  3761  ssun3  3762  elun1  3764  inabs  3839  reuun1  3891  un00  3989  snsspr1  4320  snsstp1  4322  snsstp2  4323  uniintsn  4486  sofld  5550  sssucid  5771  fvrn0  6183  ovima0  6778  unexb  6923  dmexg  7059  suppun  7275  dftpos2  7329  tpostpos2  7333  wfrlem14  7388  wfrlem15  7389  tfrlem11  7444  oaabs2  7685  ralxpmap  7867  domss2  8079  mapunen  8089  ac6sfi  8164  frfi  8165  unfir  8188  domunfican  8193  iunfi  8214  elfiun  8296  dffi3  8297  unwdomg  8449  unxpwdom2  8453  unxpwdom  8454  cantnfp1lem1  8535  cantnfp1lem3  8537  tc2  8578  unwf  8633  rankunb  8673  r0weon  8795  infxpenlem  8796  dfac2  8913  cdadom3  8970  cdainflem  8973  infunabs  8989  infcda  8990  infdif  8991  ackbij1lem15  9016  cfsmolem  9052  isfin4-3  9097  fin23lem11  9099  fin1a2lem10  9191  fin1a2lem13  9194  axdc3lem4  9235  axcclem  9239  zornn0g  9287  ttukeylem1  9291  ttukeylem5  9295  ttukeylem7  9297  fingch  9405  fpwwe2lem13  9424  gchac  9463  wunfi  9503  wundm  9510  wunex2  9520  inar1  9557  ressxr  10043  nnssnn0  11255  un0addcl  11286  un0mulcl  11287  nn0ssxnn0  11326  hashbclem  13190  hashf1lem1  13193  hashf1lem2  13194  ccatrn  13327  trclublem  13684  relexpdmg  13732  relexpaddg  13743  fsumsplit  14420  fsum2d  14449  fsumabs  14479  fsumrlim  14489  fsumo1  14490  incexclem  14512  fprodsplit  14640  fprod2d  14655  lcmfunsnlem1  15293  coprmprod  15318  vdwapid1  15622  vdwlem6  15633  ramcl2  15663  isstruct2  15809  srngbase  15949  srngplusg  15950  srngmulr  15951  lmodbase  15958  lmodplusg  15959  lmodsca  15960  ipsbase  15965  ipsaddg  15966  ipsmulr  15967  phlbase  15975  phlplusg  15976  phlsca  15977  odrngbas  16007  odrngplusg  16008  odrngmulr  16009  prdssca  16056  prdsbas  16057  prdsplusg  16058  prdsmulr  16059  prdsvsca  16060  prdsip  16061  prdsle  16062  prdsds  16064  prdstset  16066  imasbas  16112  imasplusg  16117  imasmulr  16118  imassca  16119  imasvsca  16120  imasip  16121  mreexexlem2d  16245  drsdirfi  16878  ipobas  17095  ipotset  17097  acsfiindd  17117  psdmrn  17147  dirdm  17174  gsumzsplit  18267  gsumsplit2  18269  gsumzunsnd  18295  gsum2dlem2  18310  dprdfadd  18359  dmdprdsplit2lem  18384  dmdprdsplit2  18385  dmdprdsplit  18386  dprdsplit  18387  ablfac1eulem  18411  lspun  18927  lspsolv  19083  lsppratlem3  19089  islbs3  19095  lbsextlem2  19099  lbsextlem4  19101  psrbagaddcl  19310  psrbas  19318  psrplusg  19321  psrmulr  19324  mplsubglem  19374  mplcoe1  19405  mplcoe5  19408  cnfldbas  19690  cnfldadd  19691  cnfldmul  19692  cnfldcj  19693  cnfldtset  19694  cnfldle  19695  cnfldds  19696  mdetunilem9  20366  basdif0  20697  ordtbas2  20935  ordtbas  20936  ordtopn1  20938  leordtval2  20956  iocpnfordt  20959  icomnfordt  20960  uncmp  21146  fiuncmp  21147  bwth  21153  locfincmp  21269  comppfsc  21275  1stckgenlem  21296  1stckgen  21297  ptbasin  21320  ptbasfi  21324  dfac14lem  21360  dfac14  21361  ptuncnv  21550  ptunhmeo  21551  ptcmpfi  21556  fbun  21584  trfil2  21631  ufprim  21653  ufileu  21663  filufint  21664  ufildr  21675  fmfnfm  21702  hausflim  21725  fclsfnflim  21771  alexsubALTlem4  21794  tmdgsum  21839  tsmsgsum  21882  tsmsres  21887  tsmssplit  21895  tsmsxplem1  21896  ustssco  21958  ustuqtop1  21985  prdsxmetlem  22113  prdsbl  22236  icccmplem2  22566  fsumcn  22613  cnmpt2pc  22667  rrxmetlem  23130  rrxmet  23131  rrxdstprj1  23132  ovolctb2  23200  ovolunnul  23208  ovolfiniun  23209  nulmbl2  23244  finiunmbl  23252  volfiniun  23255  icombl  23272  ioombl  23273  uniiccdif  23286  mbfres2  23352  itg2splitlem  23455  itg2split  23456  itgfsum  23533  itgsplit  23542  itgsplitioo  23544  dvreslem  23613  dvaddbr  23641  dvmulbr  23642  dvmptfsum  23676  lhop  23717  dvcnvrelem2  23719  mdegcl  23767  elplyr  23895  plyrem  23998  xrlimcnp  24629  fsumharmonic  24672  chtdif  24818  lgsdir2lem3  24986  lgsquadlem2  25040  dchrisum0lem1b  25138  pntrlog2bndlem6  25206  pntlemf  25228  ex-ss  27172  shsleji  28117  shsval2i  28134  ssjo  28194  sshhococi  28293  padct  29381  gsumle  29606  gsumvsca1  29609  gsumvsca2  29610  esumsplit  29938  esumpad2  29941  aean  30130  sxbrsigalem2  30171  bnj931  30602  subfacp1lem2b  30924  subfacp1lem3  30925  subfacp1lem5  30927  kur14lem7  30955  kur14lem9  30957  cvmliftlem10  31037  dftrpred3g  31487  refssfne  32048  filnetlem3  32070  bj-unrab  32622  bj-snglsstag  32669  bj-2upln0  32711  bj-ccssccbar  32776  finixpnum  33065  matunitlindflem1  33076  mbfresfi  33127  prdsbnd  33263  heibor1lem  33279  rrnequiv  33305  paddunssN  34613  sspadd1  34620  sspadd2  34621  pclfinN  34705  dochdmj1  36198  dvhdimlem  36252  elrfi  36776  mzpcompact2lem  36833  eldioph2  36844  eldioph4b  36894  ttac  37122  pwssplit4  37178  pwslnmlem2  37182  isnumbasgrplem2  37194  algbase  37268  algaddg  37269  algmulr  37270  fiuneneq  37295  idomsubgmo  37296  rclexi  37442  rtrclex  37444  trclubgNEW  37445  trclexi  37447  rtrclexi  37448  cnvrcl0  37452  cnvtrcl0  37453  dfrtrcl5  37456  trrelsuperrel2dg  37483  dfrcl2  37486  relexp0a  37528  relexpaddss  37530  trclimalb2  37538  frege83d  37560  frege131d  37576  dssmapnvod  37835  clsk3nimkb  37859  isotone1  37867  compneOLD  38165  mccllem  39265  cncfiooicclem1  39441  dvmptfprod  39497  dvnprodlem1  39498  iblsplit  39519  fourierdlem54  39714  fourierdlem102  39762  fourierdlem103  39763  fourierdlem104  39764  fourierdlem114  39774  sge0resplit  39960  sge0split  39963  sge0splitmpt  39965  sge0xaddlem1  39987  isomenndlem  40081  hoiprodp1  40139  hoidmvlelem1  40146  hoidmvlelem2  40147  hoidmvlelem3  40148  hoidmvlelem4  40149  gsumsplit2f  41461  setrec1lem4  41760  elpglem2  41778
  Copyright terms: Public domain W3C validator