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

Theorem ssexg 3478
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 2681 . . . 4
21imbi1d 308 . . 3
3 vex 2338 . . . 4
43ssex 3476 . . 3
52, 4vtoclg 2386 . 2
65impcom 419 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 360   wceq 1425   wcel 1427  cvv 2335   wss 2638
This theorem is referenced by:  difexg 3479  rabexg 3481  elssabg 3483  elpw2g 3484  abssexg 3510  snexALT 3511  trsuc 3765  ordsssuc2 3770  unexb 3807  difex2 3812  uniexb 3873  xpexg 4117  dmexg 4227  rnexg 4228  resexg 4276  resiexg 4279  imaexg 4304  cnvexg 4444  coexg 4451  fabexg 4592  f1oabexg 4647  resfunexgALT 4796  cofunexg 4797  fnexALT 4800  opabex2g 4804  f1dmex 4810  oprabexd 4999  oprabex2g 5001  ofres 5161  tz7.48-3 5401  oaabs 5541  mapex 5642  pmvalg 5646  elpmg 5649  pmss12g 5654  ixpexg 5683  ssdom2g 5739  cnven 5761  fiprc 5767  infensuc 5900  pssnn 5941  fival 6002  fiss 6011  wofib 6055  card2on 6057  cdainflem 6411  cofsmo 6442  inar1 6681  gruen 6718  shftfval 8870  rlim 9160  o1of2 9226  o1rlimmul 9231  summolem2 9310  ressbas2 10053  gsumval 10468  gsumval3 10478  subsubrg 10654  islbs2 10786  issubgo 10976  istps3OLD 11185  istps3 11190  tgval 11208  eltg 11210  eltg2 11211  basgen2 11233  subspval 11345  stoig2 11350  stoig 11351  subsubtop 11353  subcld 11358  subcls 11361  subntr 11362  lpval 11366  cnsubsp 11404  cnsubsp2 11405  cnpsubsp 11407  cnpsubsp2 11408  cmpcov 11429  cmpsublem 11431  cmpsub 11432  connsub 11445  cnmpt2res 11488  homeofval 11494  hmeores 11501  isfil2 11527  isfildlem 11528  flimfval 11556  subtopmet 11692  cnmptre 11778  bndth 11796  lmfval 11854  metelcls 11900  metcld2 11902  cmsss 11911  bcthlem1 11913  cnheibor 12356  ovoliunlem1 12404  mbfimaopn2 12517  cncombf 12518  0pledm 12533  dvfval 12724  dvlmlem2 12731  dvreslem 12735  dvcnp2 12741  dvcn 12742  dvaddbr 12743  dvmulbr 12744  dvadd 12745  dvmul 12746  dvaddf 12747  dvmulf 12748  dvcmulf 12750  dvcobr 12751  dvcof 12753  dvcjbr 12754  dvmptadd 12763  dvmptmul 12764  dvmptco 12774  ftc1lemf 12783  elply2 12807  plyf 12809  plyss 12810  elplyr 12812  plyeq0lem 12821  plyeq0 12822  plyaddlem 12825  plymullem 12826  dgrlem 12839  coeidlem 12847  dfon2lem3 15123  setlikess 15192  tz6.26 15204  frmin 15240  altxpexg 15516  oprabex2gpop 16057  prjmapcp 16215  prjmapcp2 16221  ubpar 16319  qusp 16646  fgsb2 16659  cnfilca 16660  trfil 16667  islimrs3 16693  islimrs4 16694  consuba 16855  uncon 16861  dualded 16940  dualcat2 16941  fnctartar3 17066  prismorcsetlem 17069  prismorcset 17071  isline1 17143  lemindclsbu 17188  indcls2 17189  cncls 17307  ivthALT 17328  topjoin 17401  fnejoin1 17404  filssufil 17448  flimcls 17464  rnelfmlem 17468  rnelfm 17469  fmfnfmlem4 17473  sfcls 17480  filnetlem3 17518  filnetlem4 17519  abrexdom 17597  sdclem2 17647  sdclem1 17648  cnres2 17678  cnresima 17679  sstotbnd 17693  totbndss 17694  ismtyval 17704  erex 17920  elmapssres 17948  brrpssg 18337  infpssss 18371  ssfin2 18384  ssfin3ds 18410  ackbij1lem11 18557  lsslss 18622  bnj74 19580  bnj1412 20651  strssd 23167
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-sep 3458
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-ex 1347  df-sb 1602  df-clab 1917  df-cleq 1922  df-clel 1925  df-v 2337  df-in 2645  df-ss 2647
Copyright terms: Public domain