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

Theorem ssun1 3969
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 885 . . 3 (𝑥𝐴 → (𝑥𝐴𝑥𝐵))
2 elun 3946 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
31, 2sylibr 225 . 2 (𝑥𝐴𝑥 ∈ (𝐴𝐵))
43ssriv 3796 1 𝐴 ⊆ (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 865  wcel 2155  cun 3761  wss 3763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-v 3389  df-un 3768  df-in 3770  df-ss 3777
This theorem is referenced by:  ssun2  3970  ssun3  3971  elun1  3973  difsssymdif  4047  inabs  4051  reuun1  4104  un00  4203  snsspr1  4529  snsstp1  4531  snsstp2  4532  uniintsn  4699  sofld  5786  sssucid  6009  fvrn0  6430  ovima0  7037  unexb  7182  dmexg  7321  suppun  7543  dftpos2  7598  tpostpos2  7602  wfrlem14  7658  wfrlem15  7659  tfrlem11  7714  oaabs2  7956  ralxpmap  8138  domss2  8352  mapunen  8362  ac6sfi  8437  frfi  8438  unfir  8461  domunfican  8466  iunfi  8487  elfiun  8569  dffi3  8570  unwdomg  8722  unxpwdom2  8726  unxpwdom  8727  cantnfp1lem1  8816  cantnfp1lem3  8818  tc2  8859  unwf  8914  rankunb  8954  r0weon  9112  infxpenlem  9113  dfac2b  9230  dfac2OLD  9232  cdadom3  9289  cdainflem  9292  infunabs  9308  infcda  9309  infdif  9310  ackbij1lem15  9335  cfsmolem  9371  isfin4-3  9416  fin23lem11  9418  fin1a2lem10  9510  fin1a2lem13  9513  axdc3lem4  9554  axcclem  9558  zornn0g  9606  ttukeylem1  9610  ttukeylem5  9614  ttukeylem7  9616  fingch  9724  fpwwe2lem13  9743  gchac  9782  wunfi  9822  wundm  9829  wunex2  9839  inar1  9876  ressxr  10362  nnssnn0  11556  un0addcl  11586  un0mulcl  11587  nn0ssxnn0  11626  hashbclem  13447  hashf1lem1  13450  hashf1lem2  13451  ccatrn  13580  trclublem  13953  relexpdmg  13999  relexpaddg  14010  fsumsplit  14688  fsum2d  14719  fsumabs  14749  fsumrlim  14759  fsumo1  14760  incexclem  14784  fprodsplit  14911  fprod2d  14926  lcmfunsnlem1  15563  coprmprod  15587  vdwapid1  15890  vdwlem6  15901  ramcl2  15931  isstruct2  16072  srngbase  16214  srngplusg  16215  srngmulr  16216  lmodbase  16223  lmodplusg  16224  lmodsca  16225  ipsbase  16230  ipsaddg  16231  ipsmulr  16232  phlbase  16240  phlplusg  16241  phlsca  16242  odrngbas  16266  odrngplusg  16267  odrngmulr  16268  prdssca  16315  prdsbas  16316  prdsplusg  16317  prdsmulr  16318  prdsvsca  16319  prdsip  16320  prdsle  16321  prdsds  16323  prdstset  16325  imasbas  16371  imasplusg  16376  imasmulr  16377  imassca  16378  imasvsca  16379  imasip  16380  mreexexlem2d  16504  drsdirfi  17137  ipobas  17354  ipotset  17356  acsfiindd  17376  psdmrn  17406  dirdm  17433  gsumzsplit  18522  gsumsplit2  18524  gsumzunsnd  18550  gsum2dlem2  18565  dprdfadd  18615  dmdprdsplit2lem  18640  dmdprdsplit2  18641  dmdprdsplit  18642  dprdsplit  18643  ablfac1eulem  18667  lspun  19188  lspsolv  19345  lsppratlem3  19352  islbs3  19358  lbsextlem2  19362  lbsextlem4  19364  psrbagaddcl  19573  psrbas  19581  psrplusg  19584  psrmulr  19587  mplsubglem  19637  mplcoe1  19668  mplcoe5  19671  cnfldbas  19952  cnfldadd  19953  cnfldmul  19954  cnfldcj  19955  cnfldtset  19956  cnfldle  19957  cnfldds  19958  mdetunilem9  20631  basdif0  20965  ordtbas2  21203  ordtbas  21204  ordtopn1  21206  leordtval2  21224  iocpnfordt  21227  icomnfordt  21228  uncmp  21414  fiuncmp  21415  bwth  21421  locfincmp  21537  comppfsc  21543  1stckgenlem  21564  1stckgen  21565  ptbasin  21588  ptbasfi  21592  dfac14lem  21628  dfac14  21629  ptuncnv  21818  ptunhmeo  21819  ptcmpfi  21824  fbun  21851  trfil2  21898  ufprim  21920  ufileu  21930  filufint  21931  ufildr  21942  fmfnfm  21969  hausflim  21992  fclsfnflim  22038  alexsubALTlem4  22061  tmdgsum  22106  tsmsgsum  22149  tsmsres  22154  tsmssplit  22162  tsmsxplem1  22163  ustssco  22225  ustuqtop1  22252  prdsxmetlem  22380  prdsbl  22503  icccmplem2  22833  fsumcn  22880  cnmpt2pc  22934  rrxmetlem  23396  rrxmet  23397  rrxdstprj1  23398  ovolctb2  23467  ovolunnul  23475  ovolfiniun  23476  nulmbl2  23511  finiunmbl  23519  volfiniun  23522  icombl  23539  ioombl  23540  uniiccdif  23553  mbfres2  23620  itg2splitlem  23723  itg2split  23724  itgfsum  23801  itgsplit  23810  itgsplitioo  23812  dvreslem  23881  dvaddbr  23909  dvmulbr  23910  dvmptfsum  23946  lhop  23987  dvcnvrelem2  23989  mdegcl  24037  elplyr  24165  plyrem  24268  xrlimcnp  24903  fsumharmonic  24946  chtdif  25092  lgsdir2lem3  25260  lgsquadlem2  25314  dchrisum0lem1b  25412  pntrlog2bndlem6  25480  pntlemf  25502  ex-ss  27609  shsleji  28551  shsval2i  28568  ssjo  28628  sshhococi  28727  padct  29818  gsumle  30098  gsumvsca1  30101  gsumvsca2  30102  esumsplit  30434  esumpad2  30437  aean  30626  sxbrsigalem2  30667  bnj931  31158  subfacp1lem2b  31480  subfacp1lem3  31481  subfacp1lem5  31483  kur14lem7  31511  kur14lem9  31513  cvmliftlem10  31593  dftrpred3g  32047  scutun12  32232  refssfne  32668  filnetlem3  32690  bj-unrab  33227  bj-snglsstag  33273  bj-2upln0  33315  bj-ccssccbar  33415  finixpnum  33701  matunitlindflem1  33712  mbfresfi  33762  prdsbnd  33897  heibor1lem  33913  rrnequiv  33939  paddunssN  35582  sspadd1  35589  sspadd2  35590  pclfinN  35674  dochdmj1  37165  dvhdimlem  37219  elrfi  37753  mzpcompact2lem  37810  eldioph2  37821  eldioph4b  37871  ttac  38098  pwssplit4  38154  pwslnmlem2  38158  isnumbasgrplem2  38169  algbase  38243  algaddg  38244  algmulr  38245  fiuneneq  38270  idomsubgmo  38271  rclexi  38416  rtrclex  38418  trclubgNEW  38419  trclexi  38421  rtrclexi  38422  cnvrcl0  38426  cnvtrcl0  38427  dfrtrcl5  38430  trrelsuperrel2dg  38457  dfrcl2  38460  relexp0a  38502  relexpaddss  38504  trclimalb2  38512  frege83d  38534  frege131d  38550  dssmapnvod  38808  clsk3nimkb  38832  isotone1  38840  compneOLD  39137  infxrpnf  40147  mccllem  40303  cncfiooicclem1  40580  dvmptfprod  40634  dvnprodlem1  40635  iblsplit  40655  fourierdlem54  40850  fourierdlem102  40898  fourierdlem103  40899  fourierdlem104  40900  fourierdlem114  40910  sge0resplit  41096  sge0split  41099  sge0splitmpt  41101  sge0xaddlem1  41123  isomenndlem  41220  hoiprodp1  41278  hoidmvlelem1  41285  hoidmvlelem2  41286  hoidmvlelem3  41287  hoidmvlelem4  41288  gsumsplit2f  42705  setrec1lem4  42999  elpglem2  43020
  Copyright terms: Public domain W3C validator