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

Theorem ssun1 3737
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 398 . . 3 (𝑥𝐴 → (𝑥𝐴𝑥𝐵))
2 elun 3714 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
31, 2sylibr 222 . 2 (𝑥𝐴𝑥 ∈ (𝐴𝐵))
43ssriv 3571 1 𝐴 ⊆ (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 381  wcel 1976  cun 3537  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-in 3546  df-ss 3553
This theorem is referenced by:  ssun2  3738  ssun3  3739  elun1  3741  inabs  3816  reuun1  3867  un00  3962  snsspr1  4284  snsstp1  4286  snsstp2  4287  uniintsn  4443  sofld  5486  sssucid  5705  fvrn0  6111  ovima0  6688  unexb  6833  dmexg  6966  suppun  7179  dftpos2  7233  tpostpos2  7237  wfrlem14  7292  wfrlem15  7293  tfrlem11  7348  oaabs2  7589  ralxpmap  7770  domss2  7981  mapunen  7991  ac6sfi  8066  frfi  8067  unfir  8090  domunfican  8095  iunfi  8114  elfiun  8196  dffi3  8197  unwdomg  8349  unxpwdom2  8353  unxpwdom  8354  cantnfp1lem1  8435  cantnfp1lem3  8437  tc2  8478  unwf  8533  rankunb  8573  r0weon  8695  infxpenlem  8696  dfac2  8813  cdadom3  8870  cdainflem  8873  infunabs  8889  infcda  8890  infdif  8891  ackbij1lem15  8916  cfsmolem  8952  isfin4-3  8997  fin23lem11  8999  fin1a2lem10  9091  fin1a2lem13  9094  axdc3lem4  9135  axcclem  9139  zornn0g  9187  ttukeylem1  9191  ttukeylem5  9195  ttukeylem7  9197  fingch  9301  fpwwe2lem13  9320  gchac  9359  wunfi  9399  wundm  9406  wunex2  9416  inar1  9453  ressxr  9939  nnssnn0  11142  un0addcl  11173  un0mulcl  11174  hashbclem  13045  hashf1lem1  13048  hashf1lem2  13049  ccatrn  13171  trclublem  13528  relexpdmg  13576  relexpaddg  13587  fsumsplit  14264  fsum2d  14290  fsumabs  14320  fsumrlim  14330  fsumo1  14331  incexclem  14353  fprodsplit  14481  fprod2d  14496  lcmfunsnlem1  15134  coprmprod  15159  vdwapid1  15463  vdwlem6  15474  ramcl2  15504  isstruct2  15650  srngbase  15778  srngplusg  15779  srngmulr  15780  lmodbase  15787  lmodplusg  15788  lmodsca  15789  ipsbase  15794  ipsaddg  15795  ipsmulr  15796  phlbase  15804  phlplusg  15805  phlsca  15806  odrngbas  15836  odrngplusg  15837  odrngmulr  15838  prdssca  15885  prdsbas  15886  prdsplusg  15887  prdsmulr  15888  prdsvsca  15889  prdsip  15890  prdsle  15891  prdsds  15893  prdstset  15895  imasbas  15941  imasplusg  15946  imasmulr  15947  imassca  15948  imasvsca  15949  imasip  15950  mreexexlem2d  16074  drsdirfi  16707  ipobas  16924  ipotset  16926  acsfiindd  16946  psdmrn  16976  dirdm  17003  gsumzsplit  18096  gsumsplit2  18098  gsumzunsnd  18124  gsum2dlem2  18139  dprdfadd  18188  dmdprdsplit2lem  18213  dmdprdsplit2  18214  dmdprdsplit  18215  dprdsplit  18216  ablfac1eulem  18240  lspun  18754  lspsolv  18910  lsppratlem3  18916  islbs3  18922  lbsextlem2  18926  lbsextlem4  18928  psrbagaddcl  19137  psrbas  19145  psrplusg  19148  psrmulr  19151  mplsubglem  19201  mplcoe1  19232  mplcoe5  19235  cnfldbas  19517  cnfldadd  19518  cnfldmul  19519  cnfldcj  19520  cnfldtset  19521  cnfldle  19522  cnfldds  19523  mdetunilem9  20187  basdif0  20510  ordtbas2  20747  ordtbas  20748  ordtopn1  20750  leordtval2  20768  iocpnfordt  20771  icomnfordt  20772  uncmp  20958  fiuncmp  20959  bwth  20965  locfincmp  21081  comppfsc  21087  1stckgenlem  21108  1stckgen  21109  ptbasin  21132  ptbasfi  21136  dfac14lem  21172  dfac14  21173  ptuncnv  21362  ptunhmeo  21363  ptcmpfi  21368  fbun  21396  trfil2  21443  ufprim  21465  ufileu  21475  filufint  21476  ufildr  21487  fmfnfm  21514  hausflim  21537  fclsfnflim  21583  alexsubALTlem4  21606  tmdgsum  21651  tsmsgsum  21694  tsmsres  21699  tsmssplit  21707  tsmsxplem1  21708  ustssco  21770  ustuqtop1  21797  prdsxmetlem  21924  prdsbl  22047  icccmplem2  22366  fsumcn  22412  cnmpt2pc  22466  rrxmetlem  22915  rrxmet  22916  rrxdstprj1  22917  ovolctb2  22984  ovolunnul  22992  ovolfiniun  22993  nulmbl2  23028  finiunmbl  23036  volfiniun  23039  icombl  23056  ioombl  23057  uniiccdif  23069  mbfres2  23135  itg2splitlem  23238  itg2split  23239  itgfsum  23316  itgsplit  23325  itgsplitioo  23327  dvreslem  23396  dvaddbr  23424  dvmulbr  23425  dvmptfsum  23459  lhop  23500  dvcnvrelem2  23502  mdegcl  23550  elplyr  23678  plyrem  23781  xrlimcnp  24412  fsumharmonic  24455  chtdif  24601  lgsdir2lem3  24769  lgsquadlem2  24823  dchrisum0lem1b  24921  pntrlog2bndlem6  24989  pntlemf  25011  ex-ss  26442  shsleji  27419  shsval2i  27436  ssjo  27496  sshhococi  27595  padct  28691  gsumle  28916  gsumvsca1  28919  gsumvsca2  28920  esumsplit  29248  esumpad2  29251  aean  29440  sxbrsigalem2  29481  bnj931  29901  subfacp1lem2b  30223  subfacp1lem3  30224  subfacp1lem5  30226  kur14lem7  30254  kur14lem9  30256  cvmliftlem10  30336  dftrpred3g  30783  nofulllem4  30910  refssfne  31329  filnetlem3  31351  bj-unrab  31917  bj-snglsstag  31965  bj-2upln0  32007  bj-ccssccbar  32084  finixpnum  32367  matunitlindflem1  32378  mbfresfi  32429  prdsbnd  32565  heibor1lem  32581  rrnequiv  32607  paddunssN  33915  sspadd1  33922  sspadd2  33923  pclfinN  34007  dochdmj1  35500  dvhdimlem  35554  elrfi  36078  mzpcompact2lem  36135  eldioph2  36146  eldioph4b  36196  ttac  36424  pwssplit4  36480  pwslnmlem2  36484  isnumbasgrplem2  36496  algbase  36570  algaddg  36571  algmulr  36572  fiuneneq  36597  idomsubgmo  36598  rclexi  36744  rtrclex  36746  trclubgNEW  36747  trclexi  36749  rtrclexi  36750  cnvrcl0  36754  cnvtrcl0  36755  dfrtrcl5  36758  trrelsuperrel2dg  36785  dfrcl2  36788  relexp0a  36830  relexpaddss  36832  trclimalb2  36840  frege83d  36862  frege131d  36878  dssmapnvod  37137  clsk3nimkb  37161  isotone1  37169  compne  37468  mccllem  38468  cncfiooicclem1  38583  dvmptfprod  38639  dvnprodlem1  38640  iblsplit  38662  fourierdlem54  38857  fourierdlem102  38905  fourierdlem103  38906  fourierdlem104  38907  fourierdlem114  38917  sge0resplit  39103  sge0split  39106  sge0splitmpt  39108  sge0xaddlem1  39130  isomenndlem  39224  hoiprodp1  39282  hoidmvlelem1  39289  hoidmvlelem2  39290  hoidmvlelem3  39291  hoidmvlelem4  39292  nn0ssxnn0  40202  gsumsplit2f  41938
  Copyright terms: Public domain W3C validator