MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssexg Unicode version

Theorem ssexg 4598
Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.)
Assertion
Ref Expression
ssexg

Proof of Theorem ssexg
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 sseq2 3525 . . . 4
21imbi1d 317 . . 3
3 vex 3112 . . . 4
43ssex 4596 . . 3
52, 4vtoclg 3167 . 2
65impcom 430 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818   cvv 3109  C_wss 3475
This theorem is referenced by:  ssexd  4599  difexg  4600  rabexg  4602  elssabg  4607  elpw2g  4615  abssexg  4637  snexALT  4638  sess1  4852  sess2  4853  trsuc  4967  ordsssuc2  4971  riinint  5264  resexg  5321  mptexg  6142  isofr2  6240  ofres  6555  brrpssg  6582  unexb  6600  xpexg  6602  difex2  6607  uniexb  6610  dmexg  6731  rnexg  6732  resiexg  6736  imaexg  6737  exse2  6739  cnvexg  6746  coexg  6751  fabexg  6756  f1oabexg  6759  resfunexgALT  6763  cofunexg  6764  fnexALT  6766  f1dmex  6770  oprabexd  6787  mpt2exxg  6874  suppfnss  6944  tposexg  6988  tz7.48-3  7128  oaabs  7312  erex  7354  mapex  7445  pmvalg  7450  elpmg  7454  elmapssres  7463  pmss12g  7465  ralxpmap  7488  ixpexg  7513  ssdomg  7581  fiprc  7617  domunsncan  7637  infensuc  7715  pssnn  7758  unbnn  7796  fodomfi  7819  fival  7892  fiss  7904  dffi3  7911  hartogslem2  7989  card2on  8001  wdomima2g  8033  unxpwdom2  8035  unxpwdom  8036  harwdom  8037  oemapvali  8124  ackbij1lem11  8631  cofsmo  8670  ssfin4  8711  fin23lem11  8718  ssfin2  8721  ssfin3ds  8731  isfin1-3  8787  hsmex3  8835  axdc2lem  8849  ac6num  8880  ttukeylem1  8910  ondomon  8959  fpwwe2lem3  9032  fpwwe2lem12  9040  fpwwe2lem13  9041  canthwe  9050  wuncss  9144  genpv  9398  genpdm  9401  hashss  12474  hashf1lem1  12504  wrdexg  12557  wrdexb  12558  shftfval  12903  o1of2  13435  o1rlimmul  13441  isercolllem2  13488  isstruct2  14641  ressabs  14695  prdsbas  14854  fnmrc  15004  mrcfval  15005  isacs1i  15054  mreacs  15055  isssc  15189  ipolerval  15786  ress0g  15949  symgbas  16405  sylow2a  16639  islbs3  17801  istps3OLD  19423  basdif0  19454  tgval  19456  eltg  19458  eltg2  19459  tgss  19470  basgen2  19491  2basgen  19492  bastop1  19495  resttopon  19662  restabs  19666  restcld  19673  restfpw  19680  restcls  19682  restntr  19683  ordtbas2  19692  ordtbas  19693  lmfval  19733  cnrest  19786  cmpcov  19889  cmpsublem  19899  cmpsub  19900  2ndcomap  19959  islocfin  20018  txss12  20106  ptrescn  20140  trfbas2  20344  trfbas  20345  isfildlem  20358  snfbas  20367  trfil1  20387  trfil2  20388  trufil  20411  ssufl  20419  hauspwpwf1  20488  ustval  20705  metrest  21027  cnheibor  21455  metcld2  21745  bcthlem1  21763  mbfimaopn2  22064  0pledm  22080  dvbss  22305  dvreslem  22313  dvres2lem  22314  dvcnp2  22323  dvaddbr  22341  dvmulbr  22342  dvcnvrelem2  22419  elply2  22593  plyf  22595  plyss  22596  elplyr  22598  plyeq0lem  22607  plyeq0  22608  plyaddlem  22612  plymullem  22613  dgrlem  22626  coeidlem  22634  ulmcn  22794  pserulm  22817  iseupa  24965  issubgo  25305  rabexgfGS  27401  abrexdomjm  27405  dmct  27537  ress1r  27779  pcmplfin  27863  metidval  27869  indval  28027  sigagenss  28149  measval  28169  erdsze2lem1  28647  erdsze2lem2  28648  cvxpcon  28687  elmsta  28908  dfon2lem3  29217  setlikess  29275  altxpexg  29628  ivthALT  30153  filnetlem3  30198  abrexdom  30221  sdclem2  30235  sdclem1  30236  elrfirn  30627  pwssplit4  31035  hbtlem1  31072  hbtlem7  31074  rabexgf  31399  dvnprodlem1  31743  dvnprodlem2  31744  ressval3d  32558  mpt2exxg2  32927  gsumlsscl  32976  lincellss  33027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator