Theorem rsp 2771

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 2715	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1794	. 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 1367   e. wcel 1756   A.wral 2710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-ral 2715

This theorem is referenced by:  rsp2  2773  rspec  2775  r19.12  2825  ralbi  2848  reupick2  3631  rspn0  3644  dfiun2g  4197  iinss2  4217  invdisj  4276  mpteq12f  4363  trss  4389  reusv1  4487  reusv2lem1  4488  reusv2lem2  4489  reusv2lem3  4490  reusv3  4495  ralxfrALT  4506  fvmptss  5777  ffnfv  5864  riota5f  6072  mpt2eq123  6140  peano5  6494  fun11iun  6532  tfr3  6850  tz7.48-1  6890  tz7.49  6892  nneneq  7486  scottex  8084  dfac2  8292  infpssrlem4  8467  fin23lem30  8503  fin23lem31  8504  hsmexlem2  8588  domtriomlem  8603  axdc3lem2  8612  axdc3lem4  8614  axdc4lem  8616  konigthlem  8724  winalim2  8855  nqereu  9090  dedekind  9525  dedekindle  9526  vdwlem9  14042  mreiincl  14526  srgi  16601  rngi  16645  lbsextlem3  17218  lbsextlem4  17219  tgcl  18549  txindis  19182  alexsubALTlem3  19596  isucn2  19829  prdsxmslem2  20079  fsumcn  20421  lebnumlem1  20508  iscmet3lem1  20777  iscmet3lem2  20778  bcthlem5  20814  ovoliunlem2  20961  mbfimaopnlem  21108  limciun  21344  ftalem3  22387  ostth3  22862  mptelee  23092  ubthlem2  24223  esumcvg  26487  prodeq2ii  27377  dfon2lem3  27549  dfon2lem7  27553  trpredmintr  27646  wfrlem4  27678  wfrlem12  27686  frr3g  27718  frrlem4  27722  frrlem11  27731  heicant  28379  neibastop1  28533  cover2  28560  upixp  28576  indexdom  28581  filbcmb  28587  mettrifi  28606  mpt2bi123f  28928  mptfcl  29009  mzpexpmpt  29034  aomclem2  29361  hbtlem5  29437  refsumcn  29705  rfcnnnub  29711  stoweidlem25  29773  stoweidlem28  29776  stoweidlem29  29777  stoweidlem31  29779  stoweidlem52  29800  stoweidlem59  29807  stoweidlem60  29808  stoweidlem62  29810  wallispilem3  29815  stirlinglem13  29834  2reu1  29963  ffnafv  30030  trintALTVD  31503  trintALT  31504  bnj228  31613  bnj1366  31710  bnj590  31790  bnj594  31792  bnj600  31799  bnj1128  31868  bnj1125  31870  bnj1145  31871  bnj1398  31912  bnj1417  31919  riotasvd  32447  glbconxN  32862  pmapglbx  33253  pmapglb2xN  33256  cdlemefr29exN  33886  cdlemk36  34397