Theorem rsp 2766

Description: Restricted specialization. (Contributed by NM, 17-Oct-1996.)

Assertion

Ref	Expression
rsp	|- ( A. x e. A ph -> ( x e. A -> ph ) )

Proof of Theorem rsp

Step	Hyp	Ref	Expression
1		df-ral 2710	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1793	. 2 |- ( A. x ( x e. A -> ph ) -> ( x e. A -> ph ) )
3	1, 2	sylbi 195	1 |- ( A. x e. A ph -> ( x e. A -> ph ) )

Syntax hints:   -> wi 4   A.wal 1360   e. wcel 1755   A.wral 2705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-ex 1590  df-ral 2710

This theorem is referenced by:  rsp2  2768  rspec  2770  r19.12  2820  ralbi  2843  reupick2  3624  rspn0  3637  dfiun2g  4190  iinss2  4210  invdisj  4269  mpteq12f  4356  trss  4382  reusv1  4480  reusv2lem1  4481  reusv2lem2  4482  reusv2lem3  4483  reusv3  4488  ralxfrALT  4499  fvmptss  5770  ffnfv  5856  riota5f  6065  mpt2eq123  6134  peano5  6488  fun11iun  6526  tfr3  6844  tz7.48-1  6884  tz7.49  6886  nneneq  7482  scottex  8080  dfac2  8288  infpssrlem4  8463  fin23lem30  8499  fin23lem31  8500  hsmexlem2  8584  domtriomlem  8599  axdc3lem2  8608  axdc3lem4  8610  axdc4lem  8612  konigthlem  8720  winalim2  8850  nqereu  9085  dedekind  9520  dedekindle  9521  vdwlem9  14032  mreiincl  14516  rngi  16592  lbsextlem3  17162  lbsextlem4  17163  tgcl  18415  txindis  19048  alexsubALTlem3  19462  isucn2  19695  prdsxmslem2  19945  fsumcn  20287  lebnumlem1  20374  iscmet3lem1  20643  iscmet3lem2  20644  bcthlem5  20680  ovoliunlem2  20827  mbfimaopnlem  20974  limciun  21210  ftalem3  22296  ostth3  22771  mptelee  22963  ubthlem2  24094  srgi  26046  esumcvg  26388  prodeq2ii  27272  dfon2lem3  27444  dfon2lem7  27448  trpredmintr  27541  wfrlem4  27573  wfrlem12  27581  frr3g  27613  frrlem4  27617  frrlem11  27626  heicant  28267  neibastop1  28421  cover2  28448  upixp  28464  indexdom  28469  filbcmb  28475  mettrifi  28494  mpt2bi123f  28816  mptfcl  28898  mzpexpmpt  28923  aomclem2  29250  hbtlem5  29326  areaquad  29434  refsumcn  29594  rfcnnnub  29600  stoweidlem25  29663  stoweidlem28  29666  stoweidlem29  29667  stoweidlem31  29669  stoweidlem52  29690  stoweidlem59  29697  stoweidlem60  29698  stoweidlem62  29700  wallispilem3  29705  stirlinglem13  29724  2reu1  29853  ffnafv  29920  trintALTVD  31315  trintALT  31316  bnj228  31425  bnj1366  31522  bnj590  31602  bnj594  31604  bnj600  31611  bnj1128  31680  bnj1125  31682  bnj1145  31683  bnj1398  31724  bnj1417  31731  riotasvd  32177  glbconxN  32592  pmapglbx  32983  pmapglb2xN  32986  cdlemefr29exN  33616  cdlemk36  34127