Theorem rsp 2830

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 2819	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1808	. 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 1377   e. wcel 1767   A.wral 2814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803

This theorem depends on definitions:  df-bi 185  df-ex 1597  df-ral 2819

This theorem is referenced by:  rspa  2831  rspec  2832  r19.21bi  2833  rsp2  2838  r19.12  2988  ralbi  2993  reupick2  3784  rspn0  3797  dfiun2g  4357  iinss2  4377  invdisj  4436  mpteq12f  4523  trss  4549  reusv1  4647  reusv2lem1  4648  reusv2lem2  4649  reusv2lem3  4650  reusv3  4655  ralxfrALT  4666  fvmptss  5956  ffnfv  6045  riota5f  6268  mpt2eq123  6338  peano5  6701  fun11iun  6741  tfr3  7065  tz7.48-1  7105  tz7.49  7107  nneneq  7697  scottex  8299  dfac2  8507  infpssrlem4  8682  fin23lem30  8718  fin23lem31  8719  hsmexlem2  8803  domtriomlem  8818  axdc3lem2  8827  axdc3lem4  8829  axdc4lem  8831  konigthlem  8939  winalim2  9070  nqereu  9303  dedekind  9739  dedekindle  9740  vdwlem9  14362  mreiincl  14847  srgi  16953  rngi  16998  lbsextlem3  17589  lbsextlem4  17590  tgcl  19237  txindis  19870  alexsubALTlem3  20284  isucn2  20517  prdsxmslem2  20767  fsumcn  21109  lebnumlem1  21196  iscmet3lem1  21465  iscmet3lem2  21466  bcthlem5  21502  ovoliunlem2  21649  mbfimaopnlem  21797  limciun  22033  ftalem3  23076  ostth3  23551  mptelee  23874  ubthlem2  25463  esumcvg  27732  prodeq2ii  28622  dfon2lem3  28794  dfon2lem7  28798  trpredmintr  28891  wfrlem4  28923  wfrlem12  28931  frr3g  28963  frrlem4  28967  frrlem11  28976  heicant  29626  neibastop1  29780  cover2  29807  upixp  29823  indexdom  29828  filbcmb  29834  mettrifi  29853  mpt2bi123f  30175  mptfcl  30256  mzpexpmpt  30281  aomclem2  30605  hbtlem5  30681  refsumcn  30983  rfcnnnub  30989  mullimc  31158  mullimcf  31165  limcrecl  31171  addlimc  31190  0ellimcdiv  31191  cncfshift  31212  cncfperiod  31217  cncficcgt0  31227  iblsplit  31284  itgsubsticclem  31293  stoweidlem25  31325  stoweidlem28  31328  stoweidlem29  31329  stoweidlem31  31331  stoweidlem52  31352  stoweidlem59  31359  stoweidlem60  31360  stoweidlem62  31362  wallispilem3  31367  stirlinglem13  31386  fourierdlem39  31446  fourierdlem73  31480  2reu1  31658  ffnafv  31723  trintALTVD  32760  trintALT  32761  bnj228  32870  bnj1366  32967  bnj590  33047  bnj594  33049  bnj600  33056  bnj1128  33125  bnj1125  33127  bnj1145  33128  bnj1398  33169  bnj1417  33176  riotasvd  33759  glbconxN  34174  pmapglbx  34565  pmapglb2xN  34568  cdlemefr29exN  35198  cdlemk36  35709