Theorem rsp 2769

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 2758	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1883	. 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 1403   e. wcel 1842   A.wral 2753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-12 1878

This theorem depends on definitions:  df-bi 185  df-ex 1634  df-ral 2758

This theorem is referenced by:  rspa  2770  rspec  2771  r19.21bi  2772  rsp2  2777  r19.12  2932  reupick2  3735  rspn0  3750  dfiun2g  4302  iinss2  4322  invdisj  4383  trss  4497  reusv1  4593  reusv2lem1  4594  reusv2lem3  4596  reusv3  4601  ralxfrALT  4609  fvmptss  5941  ffnfv  6035  riota5f  6263  mpt2eq123  6336  peano5  6706  fun11iun  6743  wfrlem4  7023  wfrlem12  7031  tfr3  7101  tz7.48-1  7144  tz7.49  7146  nneneq  7737  scottex  8334  dfac2  8542  infpssrlem4  8717  fin23lem30  8753  fin23lem31  8754  hsmexlem2  8838  domtriomlem  8853  axdc3lem2  8862  axdc3lem4  8864  konigthlem  8974  winalim2  9103  nqereu  9336  dedekind  9777  dedekindle  9778  prodeq2ii  13870  vdwlem9  14714  mreiincl  15208  srgi  17481  ringi  17529  lbsextlem3  18124  lbsextlem4  18125  tgcl  19761  txindis  20425  alexsubALTlem3  20839  prdsxmslem2  21322  fsumcn  21664  lebnumlem1  21751  iscmet3lem1  22020  iscmet3lem2  22021  ovoliunlem2  22204  mbfimaopnlem  22352  limciun  22588  ftalem3  23727  ostth3  24202  mptelee  24602  ubthlem2  26187  aciunf1lem  27932  esumcvg  28519  bnj228  29104  bnj590  29282  bnj594  29284  bnj600  29291  bnj1128  29360  bnj1125  29362  bnj1145  29363  bnj1398  29404  bnj1417  29411  dfon2lem3  29991  dfon2lem7  29995  trpredmintr  30032  frr3g  30073  frrlem4  30077  frrlem11  30086  neibastop1  30574  cover2  31466  upixp  31482  indexdom  31487  filbcmb  31493  mettrifi  31512  mpt2bi123f  31833  riotasvd  31960  glbconxN  32375  cdlemefr29exN  33401  cdlemk36  33912  mptfcl  34994  aomclem2  35343  hbtlem5  35421  trintALTVD  36691  trintALT  36692  refsumcn  36765  rfcnnnub  36771  mullimc  36971  mullimcf  36978  addlimc  37003  itgsubsticclem  37123  stoweidlem25  37156  stoweidlem52  37183  stoweidlem59  37190  stoweidlem62  37193  wallispilem3  37198  stirlinglem13  37217  fourierdlem73  37311  2reu1  37540  ffnafv  37605