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 15820  prjmapcp2 15826  ubpar 15911  qusp 16225  fgsb2 16238  cnfilca 16239  trfil 16246  islimrs3 16272  islimrs4 16273  consuba 16449  uncon 16455  dualded 16534  dualcat2 16535  fnctartar3 16655  prismorcsetlem 16658  prismorcset 16660  isline1 16732  lemindclsbu 16777  indcls2 16778  cncls 16896  ivthALT 16917  topjoin 16990  fnejoin1 16993  filssufil 17037  flimcls 17053  rnelfmlem 17057  rnelfm 17058  fmfnfmlem4 17062  sfcls 17069  filnetlem3 17107  filnetlem4 17108  abrexdom 17186  sdclem2 17236  sdclem1 17237  cnres2 17267  cnresima 17268  sstotbnd 17282  totbndss 17283  ismtyval 17293  erex 17509  elmapssres 17537  brrpssg 17927  infpssss 17961  ssfin2 17974  ssfin3ds 18000  bnj74 18953  bnj1412 20024
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