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

Theorem ssexg 3474
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 2677 . . . 4
21imbi1d 308 . . 3
3 vex 2338 . . . 4
43ssex 3472 . . 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 2634
This theorem is referenced by:  difexg 3475  rabexg 3477  elssabg 3479  elpw2g 3480  abssexg 3506  snexALT 3507  trsuc 3761  ordsssuc2 3766  unexb 3803  difex2 3808  uniexb 3869  xpexg 4113  dmexg 4223  rnexg 4224  resexg 4272  resiexg 4275  imaexg 4300  cnvexg 4439  coexg 4445  fabexg 4586  f1oabexg 4641  resfunexgALT 4789  cofunexg 4790  fnexALT 4793  opabex2g 4797  f1dmex 4803  oprabexd 4992  oprabex2g 4994  ofres 5148  tz7.48-3 5388  oaabs 5528  mapex 5629  pmvalg 5633  elpmg 5636  pmss12g 5641  ixpexg 5670  ssdom2g 5726  fiprc 5753  infensuc 5886  pssnn 5927  fival 5986  fiss 5995  wofib 6039  card2on 6041  cdainflem 6395  cofsmo 6426  inar1 6665  gruen 6702  shftfval 8852  rlim 9142  o1of2 9208  o1rlimmul 9213  summolem2 9292  islbs2 10537  issubg 10727  istps3OLD 10921  istps3 10926  tgval 10944  eltg 10946  eltg2 10947  basgen2 10969  subspval 11081  stoig2 11086  stoig 11087  subsubtop 11089  subcld 11094  subcls 11097  subntr 11098  lpval 11102  cnsubsp 11140  cnsubsp2 11141  cnpsubsp 11143  cnpsubsp2 11144  cmpcov 11165  cmpsublem 11167  cmpsub 11168  connsub 11181  cnmpt2res 11224  homeofval 11230  hmeores 11237  isfil2 11263  isfildlem 11264  flimfval 11292  subtopmet 11426  cnmptre 11512  bndth 11530  lmfval 11588  metelcls 11634  metcld2 11636  cmsss 11645  bcthlem1 11647  cnheibor 12090  ovoliunlem1 12138  mbfimaopn2 12251  cncombf 12252  0pledm 12267  dvfval 12458  dvlmlem2 12465  dvreslem 12469  dvcnp2 12475  dvcn 12476  dvaddbr 12477  dvmulbr 12478  dvadd 12479  dvmul 12480  dvaddf 12481  dvmulf 12482  dvcmulf 12484  dvcobr 12485  dvcof 12487  dvcjbr 12488  dvmptadd 12497  dvmptmul 12498  dvmptco 12508  ftc1lemf 12517  elply2 12541  plyf 12543  plyss 12544  elplyr 12546  plyeq0lem 12555  plyeq0 12556  plyaddlem 12559  plymullem 12560  dgrlem 12573  coeidlem 12581  dfon2lem3 14730  setlikess 14799  tz6.26 14811  frmin 14847  altxpexg 15123  oprabex2gpop 15664  prjmapcp 15822  prjmapcp2 15828  ubpar 15926  qusp 16253  fgsb2 16266  cnfilca 16267  trfil 16274  islimrs3 16300  islimrs4 16301  consuba 16462  uncon 16468  dualded 16547  dualcat2 16548  fnctartar3 16673  prismorcsetlem 16676  prismorcset 16678  isline1 16750  lemindclsbu 16795  indcls2 16796  cncls 16914  ivthALT 16935  topjoin 17008  fnejoin1 17011  filssufil 17055  flimcls 17071  rnelfmlem 17075  rnelfm 17076  fmfnfmlem4 17080  sfcls 17087  filnetlem3 17125  filnetlem4 17126  abrexdom 17204  sdclem2 17254  sdclem1 17255  cnres2 17285  cnresima 17286  sstotbnd 17300  totbndss 17301  ismtyval 17311  erex 17527  elmapssres 17555  brrpssg 17945  infpssss 17979  ssfin2 17992  ssfin3ds 18018  ackbij1lem11 18165  bnj74 19056  bnj1412 20127
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 3454
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 2641  df-ss 2643
Copyright terms: Public domain