Theorem rsp 3250

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

Assertion

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

Proof of Theorem rsp

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1812  df-ral 3077

This theorem is used by:  rspa  3251  rspec  3253  rsp2  3279  r19.12  3311  2reu1  3845  reupick2  4275  iuneqconst  4962  iinss2  5015  invdisj  5088  reusv1  5358  reusv2lem1  5359  reusv2lem3  5361  reusv3  5366  ralxfrALT  5376  fvmptss  7009  ffnfv  7122  riota5f  7407  mpoeq123  7494  frrlem4  8312  frrlem8  8316  frrlem10  8318  frrlem13  8321  tfr3  8412  tz7.48-1  8458  tz7.49  8460  nneneq  9226  frr3g  9765  scottexOLD  9939  setrec1lem2  9972  dfac2b  10214  infpssrlem4  10389  fin23lem30  10425  fin23lem31  10426  hsmexlem2  10510  domtriomlem  10525  axdc3lem2  10534  axdc3lem4  10536  konigthlem  10658  winalim2  10786  nqereu  11019  dedekind  11478  dedekindle  11479  prodeq2ii  16087  vdwlem9  17174  mreiincl  17773  sgrpidmnd  18935  srgdilem  20425  ringdilem  20483  lbsextlem3  21445  lbsextlem4  21446  tgcl  23294  txindis  23960  alexsubALTlem3  24375  prdsxmslem2  24855  fsumcn  25198  lebnumlem1  25289  iscmet3lem1  25619  iscmet3lem2  25620  ovoliunlem2  25831  mbfimaopnlem  25983  limciun  26221  ftalem3  27409  ostth3  27972  precsexlem10  28609  precsexlem11  28610  z12zsodd  28875  mpteleeOLD  29480  ubthlem2  31480  aciunf1lem  33305  esumcvg  34766  bnj228  35414  bnj590  35588  bnj594  35590  bnj600  35597  bnj1128  35668  bnj1125  35670  bnj1145  35671  bnj1398  35712  bnj1417  35719  dfon2lem3  36641  dfon2lem7  36645  neibastop1  37241  weiunlem  37345  mh-inf3f1  37423  unblimceq0lem  37466  unbdqndv2  37471  rdgssun  38408  ralssiun  38437  fvineqsneu  38441  fvineqsneq  38442  cover2  38756  upixp  38770  indexdom  38775  filbcmb  38781  mettrifi  38798  mpobi123f  39201  rsp3  39405  riotasvd  40120  glbconxN  40542  cdlemefr29exN  41566  cdlemk36  42077  aks4d1p7d1  43239  mptfcl  43838  aomclem2  44164  hbtlem5  44237  gneispace  45241  trintALTVD  45969  trintALT  45970  modelaxrep  46078  refsumcn  46154  rfcnnnub  46160  choicefi  46321  mullimc  46735  mullimcf  46742  addlimc  46765  itgsubsticclem  47092  stoweidlem25  47142  stoweidlem52  47169  stoweidlem59  47176  stoweidlem62  47179  wallispilem3  47184  stirlinglem13  47203  fourierdlem73  47296  ffnafv  48348  iunord  50966