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

Theorem ssexg 3646
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 2793 . . . 4
21imbi1d 306 . . 3
3 vex 2443 . . . 4
43ssex 3644 . . 3
52, 4vtoclg 2491 . 2
65impcom 415 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357   wceq 1526   wcel 1528  cvv 2440   wss 2750
This theorem is referenced by:  difexg 3647  rabexg 3649  elssabg 3651  elpw2g 3652  abssexg 3678  snexALT 3679  trsuc 3939  ordsssuc2 3944  unexb 3981  difex2 3986  uniexb 4047  xpexg 4295  dmexg 4419  rnexg 4420  resexg 4471  resiexg 4474  imaexg 4499  soex 4584  cnvexg 4658  coexg 4665  fabexg 4816  f1oabexg 4875  resfunexgALT 5042  cofunexg 5043  fnexALT 5046  opabex2g 5050  f1dmex 5056  oprabexd 5277  oprabex2g 5279  ofres 5493  brrpssg 5635  tz7.48-3 5775  oaabs 5942  mapex 6048  pmvalg 6053  elpmg 6056  pmss12g 6063  ixpexg 6102  cnven 6188  fiprc 6194  domunsncan 6214  infensuc 6340  pssnn 6379  unbnn 6405  fival 6451  fiss 6459  dffi3 6464  hartogslem2 6526  wemapso 6534  card2on 6536  wdom2d 6562  wdomd 6563  unxpwdom2 6569  unxpwdom 6570  harwdom 6571  cantnfle 6637  cantnflt 6638  cantnflt2 6639  cantnfp1lem2 6646  cantnfp1lem3 6647  oemapvali 6651  cantnflem1b 6653  cantnflem1d 6655  cantnflem1 6656  cnfcomlem 6667  cnfcom 6668  cnfcom2lem 6669  cnfcom3lem 6671  fodomnumlem 6917  ackbij1lem11 7066  cofsmo 7105  ssfin4 7146  fin23lem11 7153  ssfin2 7156  ssfin3ds 7166  isfin1-3 7222  fin1a2lem12 7247  hsmex3 7274  zorn2lem1 7349  zorn2lem4 7352  ttukeylem1 7362  ondomon 7407  fpwwe2lem2 7475  fpwwe2lem3 7476  fpwwe2lem5 7477  fpwwe2lem12 7484  fpwwe2lem13 7485  fpwwe2 7486  fpwwelem 7488  canthwelem 7493  canthwe 7494  pwfseqlem4 7504  hashfacen 9890  hashf1lem1 9891  shftfval 9904  o1of2 10268  o1rlimmul 10273  isercolllem2 10303  hashbcss 11069  strssd 11177  ressbas2 11191  ressabs 11198  divsfval 11345  ipolerval 11554  eqgfval 11856  gass 11932  symgbas 11949  sylow1lem3 11998  sylow2alem2 12014  sylow2a 12015  sylow2blem2 12017  gsumval 12087  gsumval3 12098  islbs3 12676  mplsubglem 12926  mpllsslem 12927  opsrtoslem2 12963  fnmrc 13200  mrcfval 13201  istps3OLD 13251  istps3 13256  tgval 13274  eltg 13276  eltg2 13277  tgss 13298  basgen2 13301  subtopbas 13307  restuni 13432  stoig 13433  restabs 13435  restcld 13441  restcls 13450  restntr 13451  lpval 13455  lmfval 13470  cnrest 13509  cnrest2 13510  cnpresti 13512  cnprest 13513  cnprest2 13514  cmpcov 13554  cmpsublem 13557  cmpsub 13558  consuba 13582  consubclo 13586  uncon 13590  2ndcomap 13617  1stcelcls 13656  hausmapdom 13657  1stckgenlem 13678  ptbasfi 13706  ptrescn 13739  cnmpt2res 13777  qtopval2 13791  elqtop 13792  qtoprest 13807  homeofval 13814  hmeores 13822  ptuncnv 13830  ptunhmeo 13831  isfil2 13860  isfildlem 13861  trfil1 13889  trfil2 13890  flimclslem 13940  hauspwpwdom 13943  elfm 13954  metrest 14076  cnmptre 14176  metcld2 14316  cmsss 14325  bcthlem1 14327  cncfmptc 14361  cncfcnvcn 14365  cnheibor 14368  mbfimaopn2 14575  cncombf 14576  0pledm 14591  dvvallem 14782  dvfval 14783  dvbss 14788  dvlmlem1 14790  dvlmlem2 14791  dvlm 14792  dvreslem 14799  dvres2lem 14800  dvcnp2 14809  dvcn 14810  dvnf 14815  dvnbss 14816  dvaddbr 14825  dvmulbr 14826  dvaddf 14829  dvmulf 14830  dvcmulf 14832  dvcobr 14833  dvcof 14835  dvcjbr 14836  dvmptntr 14856  dvcnvlem 14859  dvcnvrelem2 14887  dvcnvre 14888  ftc1lem3 14893  elply2 15076  plyf 15078  plyss 15079  elplyr 15081  plyeq0lem 15090  plyeq0 15091  plyaddlem 15094  plymullem 15095  dgrlem 15108  coeidlem 15116  ulmss 15216  ulmcn 15218  pserulm 15240  issubgo 16016  erdsze2lem1 18126  erdsze2lem2 18127  cvxpcon 18168  cvmliftmolem1 18204  cvmlift2lem9 18233  iseupa 18259  dfon2lem3 18520  setlikess 18588  tz6.26 18600  frmin 18636  altxpexg 18912  oprabex2gpop 19349  sndw 19428  prjmapcp 19499  prjmapcp2 19504  ubpar 19597  qusp 19919  fgsb2 19932  cnfilca 19933  islimrs3 19958  islimrs4 19959  dualded 20194  dualcat2 20195  fnctartar3 20320  prismorcsetlem 20323  prismorcset 20325  isline1 20397  lemindclsbu 20442  indcls2 20443  cncls 20558  ivthALT 20572  topjoin 20629  fnejoin1 20632  rnelfmlem 20670  rnelfm 20671  fmfnfmlem4 20675  filnetlem3 20722  filnetlem4 20723  abrexdom 20800  sdclem2 20849  sdclem1 20850  cnres2 20880  cnresima 20881  sstotbnd 20895  totbndss 20896  ismtyval 20906  erex 21122  ralxpmap 21157  riinint 21175  elrfi 21183  elrfirn 21184  elrfirn2 21185  isacs1i 21218  mreacs 21219  elmapssres 21243  pwssplit0 21723  pwssplit1 21724  pwssplit2 21725  pwssplit3 21726  pwssplit4 21727  frlmsplit2 21781  frlmsslss 21782  islinds2 21803  hbtlem1 21847  hbtlem7 21849  bnj74 22866  bnj1412 23937
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012  ax-sep 3626
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-ex 1448  df-sb 1703  df-clab 2018  df-cleq 2023  df-clel 2026  df-v 2442  df-in 2757  df-ss 2761
Copyright terms: Public domain