Theorem rsp 3245

Description: Restricted specialization. (Contributed by NM, 17-Oct-1996.)

Assertion

Ref	Expression
rsp	⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))

Proof of Theorem rsp

Step	Hyp	Ref	Expression
1		df-ral 3063	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		sp 2177	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑))
3	1, 2	sylbi 216	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-ral 3063

This theorem is referenced by:  rspa  3246  rspec  3248  rsp2  3275  r19.12  3312  r19.12OLD  3313  2reu1  3892  reupick2  4321  rspn0OLD  4354  iuneqconst  5009  iinss2  5061  invdisj  5133  reusv1  5396  reusv2lem1  5397  reusv2lem3  5399  reusv3  5404  ralxfrALT  5414  fvmptss  7011  ffnfv  7118  riota5f  7394  mpoeq123  7481  peano5OLD  7885  frrlem4  8274  frrlem8  8278  frrlem10  8280  frrlem13  8283  wfrlem4OLD  8312  wfrlem12OLD  8320  tfr3  8399  tz7.48-1  8443  tz7.49  8445  nneneq  9209  nneneqOLD  9221  frr3g  9751  scottex  9880  dfac2b  10125  infpssrlem4  10301  fin23lem30  10337  fin23lem31  10338  hsmexlem2  10422  domtriomlem  10437  axdc3lem2  10446  axdc3lem4  10448  konigthlem  10563  winalim2  10691  nqereu  10924  dedekind  11377  dedekindle  11378  prodeq2ii  15857  vdwlem9  16922  mreiincl  17540  sgrpidmnd  18630  srgdilem  20015  ringdilem  20072  lbsextlem3  20773  lbsextlem4  20774  tgcl  22472  txindis  23138  alexsubALTlem3  23553  prdsxmslem2  24038  fsumcn  24386  lebnumlem1  24477  iscmet3lem1  24808  iscmet3lem2  24809  ovoliunlem2  25020  mbfimaopnlem  25172  limciun  25411  ftalem3  26579  ostth3  27141  precsexlem10  27662  precsexlem11  27663  mptelee  28153  ubthlem2  30124  aciunf1lem  31887  esumcvg  33084  bnj228  33746  bnj590  33921  bnj594  33923  bnj600  33930  bnj1128  34001  bnj1125  34003  bnj1145  34004  bnj1398  34045  bnj1417  34052  dfon2lem3  34757  dfon2lem7  34761  neibastop1  35244  unblimceq0lem  35382  unbdqndv2  35387  rdgssun  36259  ralssiun  36288  fvineqsneu  36292  fvineqsneq  36293  cover2  36583  upixp  36597  indexdom  36602  filbcmb  36608  mettrifi  36625  mpobi123f  37030  riotasvd  37826  glbconxN  38249  cdlemefr29exN  39273  cdlemk36  39784  aks4d1p7d1  40947  mptfcl  41458  aomclem2  41797  hbtlem5  41870  gneispace  42885  trintALTVD  43641  trintALT  43642  refsumcn  43714  rfcnnnub  43720  choicefi  43899  mullimc  44332  mullimcf  44339  addlimc  44364  itgsubsticclem  44691  stoweidlem25  44741  stoweidlem52  44768  stoweidlem59  44775  stoweidlem62  44778  wallispilem3  44783  stirlinglem13  44802  fourierdlem73  44895  natlocalincr  45590  ffnafv  45879  iunord  47721  setrec1lem2  47733