Theorem rsp 2754

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 2742	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1937	. 2 |- ( A. x ( x e. A -> ph ) -> ( x e. A -> ph ) )
3	1, 2	sylbi 199	1 |- ( A. x e. A ph -> ( x e. A -> ph ) )

Syntax hints:   -> wi 4   A.wal 1442   e. wcel 1887   A.wral 2737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-12 1933

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-ral 2742

This theorem is referenced by:  rspa  2755  rspec  2756  r19.21bi  2757  rsp2  2762  r19.12  2916  reupick2  3729  rspn0  3744  dfiun2g  4310  iinss2  4330  invdisj  4391  trss  4506  reusv1  4603  reusv2lem1  4604  reusv2lem3  4606  reusv3  4611  ralxfrALT  4619  fvmptss  5958  ffnfv  6049  riota5f  6276  mpt2eq123  6350  peano5  6716  fun11iun  6753  wfrlem4  7039  wfrlem12  7047  tfr3  7117  tz7.48-1  7160  tz7.49  7162  nneneq  7755  scottex  8356  dfac2  8561  infpssrlem4  8736  fin23lem30  8772  fin23lem31  8773  hsmexlem2  8857  domtriomlem  8872  axdc3lem2  8881  axdc3lem4  8883  konigthlem  8993  winalim2  9121  nqereu  9354  dedekind  9797  dedekindle  9798  prodeq2ii  13967  vdwlem9  14939  mreiincl  15502  srgi  17745  ringi  17793  lbsextlem3  18383  lbsextlem4  18384  tgcl  19985  txindis  20649  alexsubALTlem3  21064  prdsxmslem2  21544  fsumcn  21902  lebnumlem1  21989  lebnumlem1OLD  21992  iscmet3lem1  22261  iscmet3lem2  22262  ovoliunlem2  22456  mbfimaopnlem  22611  limciun  22849  ftalem3  23999  ostth3  24476  mptelee  24925  ubthlem2  26513  aciunf1lem  28264  esumcvg  28907  bnj228  29543  bnj590  29721  bnj594  29723  bnj600  29730  bnj1128  29799  bnj1125  29801  bnj1145  29802  bnj1398  29843  bnj1417  29850  dfon2lem3  30431  dfon2lem7  30435  trpredmintr  30472  frr3g  30513  frrlem4  30517  frrlem11  30526  neibastop1  31015  cover2  32040  upixp  32056  indexdom  32061  filbcmb  32067  mettrifi  32086  mpt2bi123f  32406  riotasvd  32528  glbconxN  32943  cdlemefr29exN  33969  cdlemk36  34480  mptfcl  35562  aomclem2  35913  hbtlem5  35987  trintALTVD  37277  trintALT  37278  refsumcn  37351  rfcnnnub  37357  choicefi  37481  mullimc  37696  mullimcf  37703  addlimc  37729  itgsubsticclem  37852  stoweidlem25  37885  stoweidlem52  37913  stoweidlem59  37920  stoweidlem62  37923  stoweidlem62OLD  37924  wallispilem3  37929  stirlinglem13  37948  fourierdlem73  38043  2reu1  38607  ffnafv  38673