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

Theorem ssexg 3499
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 2679 . . . 4
21imbi1d 306 . . 3
3 vex 2329 . . . 4
43ssex 3497 . . 3
52, 4vtoclg 2377 . 2
65impcom 415 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357   wceq 1414   wcel 1416  cvv 2326   wss 2636
This theorem is referenced by:  difexg 3500  rabexg 3502  elssabg 3504  elpw2g 3505  abssexg 3531  snexALT 3532  trsuc 3789  ordsssuc2 3794  unexb 3831  difex2 3836  uniexb 3897  xpexg 4144  dmexg 4267  rnexg 4268  resexg 4317  resiexg 4320  imaexg 4345  cnvexg 4493  coexg 4500  fabexg 4646  f1oabexg 4702  resfunexgALT 4860  cofunexg 4861  fnexALT 4864  opabex2g 4868  f1dmex 4874  oprabexd 5071  oprabex2g 5073  ofres 5270  tz7.48-3 5523  oaabs 5664  mapex 5769  pmvalg 5773  elpmg 5776  pmss12g 5783  ixpexg 5815  ssdom2g 5874  cnven 5900  fiprc 5906  infensuc 6048  pssnn 6090  fival 6155  fiss 6163  dffi3 6168  wofib 6210  wemapso 6216  card2on 6219  cdainflem 6576  ackbij1lem11 6595  cofsmo 6634  inar1 6872  gruen 6908  hashfacen 9089  hashfaclem 9090  shftfval 9101  rlim 9396  o1of2 9462  o1rlimmul 9467  isercolllem2 9497  summolem2 9555  strssd 10317  ressbas2 10330  divsfval 10483  subsubg 10874  eqgfval 10894  gass 10942  orbsta2 10955  symgbas 10959  gsumval 11026  gsumval3 11036  subsubrg 11230  lsslss 11338  islbs3 11504  issubgo 11628  istps3OLD 11812  istps3 11817  tgval 11835  eltg 11837  eltg2 11838  tgss 11859  basgen2 11862  subtopbas 11868  subspval 11983  subspuni 11990  stoig 11991  subsubtop 11993  subcld 11999  subcls 12008  subntr 12009  lpval 12013  lmfval 12028  cnsubsp 12067  cnsubsp2 12068  cnpsubspi 12070  cnpsubsp 12071  cnpsubsp2 12072  cmpcov 12112  cmpsublem 12115  cmpsub 12116  consuba 12140  consubclo 12144  uncon 12148  2ndcdisj2 12174  2ndcomap 12175  1stcelcls 12213  hausmapdom 12214  1stckgenlem 12235  ptbasfi 12263  ptrescn 12296  cnmpt2res 12334  qtopval2 12348  elqtop 12349  qtopsubsp 12364  homeofval 12371  hmeores 12378  ptuncnv 12386  ptunhmeo 12387  isfil2 12416  isfildlem 12417  trfil1 12444  trfil2 12445  flimclslem 12468  hauspwpwdom 12471  elfm 12482  met2ndci 12602  subtopmet 12604  cnmptre 12704  metelcls 12842  metcld2 12844  cmsss 12853  bcthlem1 12855  cncfmptc 13296  cncfcnvcn 13300  cnheibor 13303  ovolctb 13347  ovoliunlem1 13358  uniiccdif 13430  dyadmbl 13450  mbfimaopn2 13507  cncombf 13508  0pledm 13523  dvfval 13714  dvbss 13719  dvlmlem1 13721  dvlmlem2 13722  dvlm 13723  dvreslem 13730  dvres2lem 13731  dvcnp2 13740  dvcn 13741  dvnf 13746  dvnbss 13747  dvaddbr 13756  dvmulbr 13757  dvaddf 13760  dvmulf 13761  dvcmulf 13763  dvcobr 13764  dvcof 13766  dvcjbr 13767  dvmptntr 13787  dvcnvlem 13790  dvcnvrelem2 13818  dvcnvre 13819  ftc1lem3 13823  elply2 13847  plyf 13849  plyss 13850  elplyr 13852  plyeq0lem 13861  plyeq0 13862  plyaddlem 13865  plymullem 13866  dgrlem 13879  coeidlem 13887  ulmval 13972  ulmss 13987  ulmcn 13989  pserulm 14009  psercn2 14010  sylow1lem3 16058  sylow2alem2 16074  sylow2a 16075  erdsze2lem1 16127  erdsze2lem2 16128  cvxpcon 16217  cvmliftmolem1 16251  iseupa 16290  mplsubglem 16507  mpllsslem 16508  dfon2lem3 16760  setlikess 16829  tz6.26 16841  frmin 16877  altxpexg 17153  oprabex2gpop 17693  prjmapcp 17843  prjmapcp2 17848  ubpar 17941  qusp 18263  fgsb2 18276  cnfilca 18277  islimrs3 18305  islimrs4 18306  dualded 18542  dualcat2 18543  fnctartar3 18668  prismorcsetlem 18671  prismorcset 18673  isline1 18745  lemindclsbu 18790  indcls2 18791  cncls 18906  ivthALT 18920  topjoin 18977  fnejoin1 18980  filssufil 19024  rnelfmlem 19038  rnelfm 19039  fmfnfmlem4 19043  filnetlem3 19090  filnetlem4 19091  abrexdom 19169  sdclem2 19219  sdclem1 19220  cnres2 19250  cnresima 19251  sstotbnd 19265  totbndss 19266  ismtyval 19276  erex 19486  domunsncan 19554  riinint 19571  elrfi 19579  elrfirn 19580  elrfirn2 19581  wdom2d 19609  wdomd 19610  hsmex3 19638  ipolerval 19662  fnmrc 19698  mrcfval 19699  elmapssres 19747  brrpssg 20179  infpssss 20211  ssfin2 20224  ssfin3ds 20248  pwssplit0 20442  pwssplit1 20443  pwssplit2 20444  pwssplit3 20445  pwssplit4 20446  frlmsplit2 20529  frlmsslss 20530  islinds2 20557  bnj74 21577  bnj1412 22648
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 3479
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 2328  df-in 2643  df-ss 2647
Copyright terms: Public domain