Theorem rsp 2929

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 2917	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 2053	. 2 |- ( A. x ( x e. A -> ph ) -> ( x e. A -> ph ) )
3	1, 2	sylbi 207	1 |- ( A. x e. A ph -> ( x e. A -> ph ) )

Syntax hints:   -> wi 4   A.wal 1481   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-ral 2917

This theorem is referenced by:  rspa  2930  rspec  2931  r19.21bi  2932  rsp2  2936  r19.12  3063  reupick2  3913  rspn0  3934  dfiun2g  4552  iinss2  4572  invdisj  4638  trssOLD  4762  reusv1  4866  reusv1OLD  4867  reusv2lem1  4868  reusv2lem3  4871  reusv3  4876  ralxfrALT  4887  fvmptss  6292  ffnfv  6388  riota5f  6636  mpt2eq123  6714  peano5  7089  fun11iun  7126  wfrlem4  7418  wfrlem12  7426  tfr3  7495  tz7.48-1  7538  tz7.49  7540  nneneq  8143  scottex  8748  dfac2  8953  infpssrlem4  9128  fin23lem30  9164  fin23lem31  9165  hsmexlem2  9249  domtriomlem  9264  axdc3lem2  9273  axdc3lem4  9275  konigthlem  9390  winalim2  9518  nqereu  9751  dedekind  10200  dedekindle  10201  prodeq2ii  14643  vdwlem9  15693  mreiincl  16256  srgi  18511  ringi  18560  lbsextlem3  19160  lbsextlem4  19161  tgcl  20773  txindis  21437  alexsubALTlem3  21853  prdsxmslem2  22334  fsumcn  22673  lebnumlem1  22760  iscmet3lem1  23089  iscmet3lem2  23090  ovoliunlem2  23271  mbfimaopnlem  23422  limciun  23658  ftalem3  24801  ostth3  25327  mptelee  25775  ubthlem2  27727  aciunf1lem  29462  esumcvg  30148  bnj228  30803  bnj590  30980  bnj594  30982  bnj600  30989  bnj1128  31058  bnj1125  31060  bnj1145  31061  bnj1398  31102  bnj1417  31109  dfon2lem3  31690  dfon2lem7  31694  trpredmintr  31731  frr3g  31779  frrlem4  31783  frrlem11  31792  sslttr  31914  neibastop1  32354  unblimceq0lem  32497  unbdqndv2  32502  cover2  33508  upixp  33524  indexdom  33529  filbcmb  33535  mettrifi  33553  mpt2bi123f  33971  riotasvd  34242  glbconxN  34664  cdlemefr29exN  35690  cdlemk36  36201  mptfcl  37283  aomclem2  37625  hbtlem5  37698  gneispace  38432  trintALTVD  39116  trintALT  39117  refsumcn  39189  rfcnnnub  39195  choicefi  39392  mullimc  39848  mullimcf  39855  addlimc  39880  itgsubsticclem  40191  stoweidlem25  40242  stoweidlem52  40269  stoweidlem59  40276  stoweidlem62  40279  wallispilem3  40284  stirlinglem13  40303  fourierdlem73  40396  2reu1  41186  ffnafv  41251  iunord  42422  setrec1lem2  42435