HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem ssexg 3511
Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized).
Assertion
Ref Expression
ssexg

Proof of Theorem ssexg
StepHypRef Expression
1 sseq2 2680 . . . 4
21imbi1d 306 . . 3
3 vex 2330 . . . 4
43ssex 3509 . . 3
52, 4vtoclg 2378 . 2
65impcom 415 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357   wceq 1414   wcel 1416  cvv 2327   wss 2637
This theorem is referenced by:  difexg 3512  rabexg 3514  elssabg 3516  elpw2g 3517  abssexg 3543  snexALT 3544  trsuc 3802  ordsssuc2 3807  unexb 3844  difex2 3849  uniexb 3910  xpexg 4157  dmexg 4281  rnexg 4282  resexg 4331  resiexg 4334  imaexg 4359  soex 4406  cnvexg 4515  coexg 4522  fabexg 4670  f1oabexg 4728  resfunexgALT 4883  cofunexg 4884  fnexALT 4887  opabex2g 4891  f1dmex 4897  oprabexd 5102  oprabex2g 5104  ofres 5307  tz7.48-3 5560  oaabs 5701  mapex 5806  pmvalg 5811  elpmg 5814  pmss12g 5821  ixpexg 5854  cnven 5935  fiprc 5941  infensuc 6079  pssnn 6117  unbnn 6143  fival 6186  fiss 6194  dffi3 6199  wofib 6243  wemapso 6249  card2on 6252  fodomnumlem 6569  ackbij1lem11 6653  cofsmo 6692  hashfacen 9232  hashf1lem1 9233  shftfval 9246  o1of2 9610  o1rlimmul 9615  isercolllem2 9645  hashbcss 10405  strssd 10513  ressbas2 10526  divsfval 10676  subsubg 11091  eqgfval 11111  gass 11163  symgbas 11180  gsumval 11250  gsumval3 11260  subsubrg 11472  lsslss 11584  islbs3 11760  issubgo 11884  istps3OLD 12066  istps3 12071  tgval 12089  eltg 12091  eltg2 12092  tgss 12113  basgen2 12116  subtopbas 12122  restuni 12244  stoig 12245  restabs 12247  restcld 12253  restcls 12262  restntr 12263  lpval 12267  lmfval 12282  cnrest 12321  cnrest2 12322  cnpresti 12324  cnprest 12325  cnprest2 12326  cmpcov 12366  cmpsublem 12369  cmpsub 12370  consuba 12394  consubclo 12398  uncon 12402  2ndcomap 12429  1stcelcls 12468  hausmapdom 12469  1stckgenlem 12490  ptbasfi 12518  ptrescn 12551  cnmpt2res 12589  qtopval2 12603  elqtop 12604  qtoprest 12619  homeofval 12626  hmeores 12633  ptuncnv 12641  ptunhmeo 12642  isfil2 12671  isfildlem 12672  trfil1 12699  trfil2 12700  flimclslem 12723  hauspwpwdom 12726  elfm 12737  metrest 12859  cnmptre 12959  metcld2 13099  cmsss 13108  bcthlem1 13110  cncfmptc 13546  cncfcnvcn 13550  cnheibor 13553  mbfimaopn2 13757  cncombf 13758  0pledm 13773  dvvallem 13964  dvfval 13965  dvbss 13970  dvlmlem1 13972  dvlmlem2 13973  dvlm 13974  dvreslem 13981  dvres2lem 13982  dvcnp2 13991  dvcn 13992  dvnf 13997  dvnbss 13998  dvaddbr 14007  dvmulbr 14008  dvaddf 14011  dvmulf 14012  dvcmulf 14014  dvcobr 14015  dvcof 14017  dvcjbr 14018  dvmptntr 14038  dvcnvlem 14041  dvcnvrelem2 14069  dvcnvre 14070  ftc1lem3 14074  elply2 14098  plyf 14100  plyss 14101  elplyr 14103  plyeq0lem 14112  plyeq0 14113  plyaddlem 14116  plymullem 14117  dgrlem 14130  coeidlem 14138  ulmss 14238  ulmcn 14240  pserulm 14260  mplsubglem 14927  mpllsslem 14928  sylow1lem3 16576  sylow2alem2 16592  sylow2a 16593  sylow2blem2 16595  erdsze2lem1 16645  erdsze2lem2 16646  cvxpcon 16735  cvmliftmolem1 16769  iseupa 16808  dfon2lem3 17074  setlikess 17143  tz6.26 17155  frmin 17191  altxpexg 17467  oprabex2gpop 18007  sndw 18086  prjmapcp 18157  prjmapcp2 18162  ubpar 18255  qusp 18577  fgsb2 18590  cnfilca 18591  islimrs3 18618  islimrs4 18619  dualded 18854  dualcat2 18855  fnctartar3 18980  prismorcsetlem 18983  prismorcset 18985  isline1 19057  lemindclsbu 19102  indcls2 19103  cncls 19218  ivthALT 19232  topjoin 19289  fnejoin1 19292  filssufil 19336  rnelfmlem 19350  rnelfm 19351  fmfnfmlem4 19355  filnetlem3 19402  filnetlem4 19403  abrexdom 19480  sdclem2 19529  sdclem1 19530  cnres2 19560  cnresima 19561  sstotbnd 19575  totbndss 19576  ismtyval 19586  erex 19796  ralxpmap 19864  domunsncan 19895  riinint 19928  elrfi 19936  elrfirn 19937  elrfirn2 19938  wdom2d 19964  wdomd 19965  hsmex3 19993  ipolerval 20017  fnmrc 20058  mrcfval 20059  isacs1i 20117  mreacs 20118  elmapssres 20148  brrpssg 20582  ssfin2 20626  ssfin3ds 20650  pwssplit0 20846  pwssplit1 20847  pwssplit2 20848  pwssplit3 20849  pwssplit4 20850  frlmsplit2 21243  frlmsslss 21244  islinds2 21265  hbtlem1 21309  hbtlem7 21311  bnj74 22270  bnj1412 23341
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-sep 3491
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-ex 1336  df-sb 1591  df-clab 1906  df-cleq 1911  df-clel 1914  df-v 2329  df-in 2644  df-ss 2648
Copyright terms: Public domain