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 2675 . . . 4
21imbi1d 305 . . 3
3 vex 2325 . . . 4
43ssex 3472 . . 3
52, 4vtoclg 2373 . 2
65impcom 414 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 356   wceq 1413   wcel 1415  cvv 2322   wss 2632
This theorem is referenced by:  difexg 3475  rabexg 3477  elssabg 3479  elpw2g 3480  abssexg 3506  snexALT 3507  trsuc 3763  ordsssuc2 3768  unexb 3805  difex2 3810  uniexb 3871  xpexg 4118  dmexg 4235  rnexg 4236  resexg 4284  resiexg 4287  imaexg 4312  cnvexg 4454  coexg 4461  fabexg 4602  f1oabexg 4658  resfunexgALT 4808  cofunexg 4809  fnexALT 4812  opabex2g 4816  f1dmex 4822  oprabexd 5012  oprabex2g 5014  ofres 5205  tz7.48-3 5449  oaabs 5589  mapex 5694  pmvalg 5698  elpmg 5701  pmss12g 5706  ixpexg 5738  ssdom2g 5794  cnven 5817  fiprc 5823  infensuc 5957  pssnn 5998  fival 6062  fiss 6071  wofib 6115  card2on 6117  cdainflem 6472  ackbij1lem11 6491  cofsmo 6529  inar1 6767  gruen 6803  hashfacen 8954  hashfaclem 8955  shftfval 8965  rlim 9255  o1of2 9321  o1rlimmul 9326  summolem2 9405  strssd 10151  ressbas2 10164  subsubg 10638  eqgfval 10655  gass 10700  orbsta2 10713  symgbas 10717  elsymgbas 10718  gsumval 10777  gsumval3 10787  subsubrg 10980  lsslss 11081  islbs3 11221  issubgo 11345  istps3OLD 11529  istps3 11534  tgval 11552  eltg 11554  eltg2 11555  tgss 11574  basgen2 11577  subspval 11689  stoig2 11694  stoig 11695  subsubtop 11697  subcld 11702  subcls 11705  subntr 11706  lpval 11710  cnsubsp 11748  cnsubsp2 11749  cnpsubsp 11751  cnpsubsp2 11752  cmpcov 11773  cmpsublem 11775  cmpsub 11776  connsub 11789  cnmpt2res 11832  homeofval 11838  hmeores 11845  isfil2 11871  isfildlem 11872  flimfval 11900  subtopmet 12033  cnmptre 12119  bndth 12137  lmfval 12195  metelcls 12241  metcld2 12243  cmsss 12252  bcthlem1 12254  cnheibor 12697  ovoliunlem1 12745  mbfimaopn2 12858  cncombf 12859  0pledm 12874  dvfval 13065  dvlmlem2 13072  dvreslem 13076  dvcnp2 13082  dvcn 13083  dvaddbr 13084  dvmulbr 13085  dvadd 13086  dvmul 13087  dvaddf 13088  dvmulf 13089  dvcmulf 13091  dvcobr 13092  dvcof 13094  dvcjbr 13095  dvmptadd 13104  dvmptmul 13105  dvmptco 13115  ftc1lemf 13124  elply2 13148  plyf 13150  plyss 13151  elplyr 13153  plyeq0lem 13162  plyeq0 13163  plyaddlem 13166  plymullem 13167  dgrlem 13180  coeidlem 13188  sylow1lem3 15166  sylow2alem2 15182  sylow2a 15183  erdsze2lem1 15235  erdsze2lem2 15236  mplsubglem 15419  mpllsslem 15420  dfon2lem3 15648  setlikess 15717  tz6.26 15729  frmin 15765  altxpexg 16041  oprabex2gpop 16582  prjmapcp 16740  prjmapcp2 16746  ubpar 16844  qusp 17169  fgsb2 17182  cnfilca 17183  trfil 17190  islimrs3 17216  islimrs4 17217  consuba 17378  uncon 17384  dualded 17463  dualcat2 17464  fnctartar3 17589  prismorcsetlem 17592  prismorcset 17594  isline1 17666  lemindclsbu 17711  indcls2 17712  cncls 17830  ivthALT 17851  topjoin 17924  fnejoin1 17927  filssufil 17971  flimcls 17987  rnelfmlem 17991  rnelfm 17992  fmfnfmlem4 17996  sfcls 18003  filnetlem3 18041  filnetlem4 18042  abrexdom 18120  sdclem2 18170  sdclem1 18171  cnres2 18201  cnresima 18202  sstotbnd 18216  totbndss 18217  ismtyval 18227  erex 18443  elmapssres 18471  wemapso 18880  brrpssg 18922  infpssss 18956  ssfin2 18969  ssfin3ds 18995  pwssplit0 19207  pwssplit1 19208  pwssplit2 19209  pwssplit3 19210  pwssplit4 19211  bnj74 20232  bnj1412 21303
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-sep 3454
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-ex 1335  df-sb 1590  df-clab 1905  df-cleq 1910  df-clel 1913  df-v 2324  df-in 2639  df-ss 2641
Copyright terms: Public domain