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

Theorem ssexg 3486
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 306 . . 3
3 vex 2327 . . . 4
43ssex 3484 . . 3
52, 4vtoclg 2375 . 2
65impcom 415 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357   wceq 1414   wcel 1416  cvv 2324   wss 2634
This theorem is referenced by:  difexg 3487  rabexg 3489  elssabg 3491  elpw2g 3492  abssexg 3518  snexALT 3519  trsuc 3775  ordsssuc2 3780  unexb 3817  difex2 3822  uniexb 3883  xpexg 4130  dmexg 4250  rnexg 4251  resexg 4300  resiexg 4303  imaexg 4328  cnvexg 4476  coexg 4483  fabexg 4628  f1oabexg 4684  resfunexgALT 4842  cofunexg 4843  fnexALT 4846  opabex2g 4850  f1dmex 4856  oprabexd 5048  oprabex2g 5050  ofres 5243  tz7.48-3 5493  oaabs 5634  mapex 5739  pmvalg 5743  elpmg 5746  pmss12g 5753  ixpexg 5785  ssdom2g 5844  cnven 5867  fiprc 5873  infensuc 6012  pssnn 6053  fival 6118  fiss 6127  wofib 6171  wemapso 6177  card2on 6180  cdainflem 6535  ackbij1lem11 6554  cofsmo 6592  inar1 6830  gruen 6866  hashfacen 9020  hashfaclem 9021  shftfval 9031  rlim 9321  o1of2 9387  o1rlimmul 9392  summolem2 9471  strssd 10218  ressbas2 10231  subsubg 10724  eqgfval 10744  gass 10792  orbsta2 10805  symgbas 10809  gsumval 10870  gsumval3 10880  subsubrg 11074  lsslss 11177  islbs3 11321  issubgo 11445  istps3OLD 11629  istps3 11634  tgval 11652  eltg 11654  eltg2 11655  tgss 11674  basgen2 11677  subspval 11789  stoig2 11794  stoig 11795  subsubtop 11797  subcld 11802  subcls 11805  subntr 11806  lpval 11810  cnsubsp 11851  cnsubsp2 11852  cnpsubspi 11854  cnpsubsp 11855  cnpsubsp2 11856  cmpcov 11877  cmpsublem 11879  cmpsub 11880  connsub 11898  consuba 11901  ptbasfi 11922  ptrescn 11945  cnmpt2res 11968  homeofval 11974  hmeores 11981  ptuncnv 11986  ptunhmeo 11987  isfil2 12012  isfildlem 12013  flimfval 12041  subtopmet 12174  cnmptre 12267  bndth 12285  lmfval 12360  metelcls 12406  metcld2 12408  cmsss 12417  bcthlem1 12419  cnheibor 12862  ovoliunlem1 12910  mbfimaopn2 13023  cncombf 13024  0pledm 13039  dvfval 13230  dvbss 13235  dvlmlem1 13236  dvlmlem2 13237  dvlm 13238  dvreslem 13245  dvres2lem 13246  dvcnp2 13255  dvcn 13256  dvnf 13261  dvnbss 13262  dvaddbr 13271  dvmulbr 13272  dvaddf 13275  dvmulf 13276  dvcmulf 13278  dvcobr 13279  dvcof 13281  dvcjbr 13282  dvmptadd 13291  dvmptmul 13292  dvmptntr 13301  dvmptco 13302  ftc1lem3 13314  elply2 13338  plyf 13340  plyss 13341  elplyr 13343  plyeq0lem 13352  plyeq0 13353  plyaddlem 13356  plymullem 13357  dgrlem 13370  coeidlem 13378  sylow1lem3 15366  sylow2alem2 15382  sylow2a 15383  erdsze2lem1 15435  erdsze2lem2 15436  cvxpcon 15520  mplsubglem 15746  mpllsslem 15747  dfon2lem3 15999  setlikess 16068  tz6.26 16080  frmin 16116  altxpexg 16392  oprabex2gpop 16932  prjmapcp 17087  prjmapcp2 17092  ubpar 17185  qusp 17510  fgsb2 17523  cnfilca 17524  trfil 17531  islimrs3 17557  islimrs4 17558  uncon 17722  dualded 17801  dualcat2 17802  fnctartar3 17927  prismorcsetlem 17930  prismorcset 17932  isline1 18004  lemindclsbu 18049  indcls2 18050  cncls 18167  ivthALT 18181  topjoin 18254  fnejoin1 18257  filssufil 18301  flimcls 18317  rnelfmlem 18321  rnelfm 18322  fmfnfmlem4 18326  sfcls 18333  filnetlem3 18371  filnetlem4 18372  abrexdom 18450  sdclem2 18500  sdclem1 18501  cnres2 18531  cnresima 18532  sstotbnd 18546  totbndss 18547  ismtyval 18557  erex 18767  domunsncan 18836  riinint 18857  elrfi 18865  elrfirn 18866  elrfirn2 18867  wdom2d 18895  wdomd 18896  hsmex3 18924  ipolerval 18948  fnmrc 18984  mrcfval 18985  elmapssres 19033  brrpssg 19468  infpssss 19502  ssfin2 19515  ssfin3ds 19539  pwssplit0 19736  pwssplit1 19737  pwssplit2 19738  pwssplit3 19739  pwssplit4 19740  frlmsplit2 19823  frlmsslss 19824  islinds2 19851  bnj74 20848  bnj1412 21919
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 3466
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 2326  df-in 2641  df-ss 2645
Copyright terms: Public domain