Theorem rsp 3205

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2114  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-ral 3143

This theorem is referenced by:  rspa  3206  rspec  3207  r19.21biOLD  3209  rsp2  3213  r19.12  3324  r19.12OLD  3327  2reu1  3881  reupick2  4289  rspn0  4313  iuneqconst  4930  dfiun2gOLD  4956  iinss2  4981  invdisj  5050  reusv1  5298  reusv2lem1  5299  reusv2lem3  5301  reusv3  5306  ralxfrALT  5316  fvmptss  6780  ffnfv  6882  riota5f  7142  mpoeq123  7226  peano5  7605  wfrlem4  7958  wfrlem12  7966  tfr3  8035  tz7.48-1  8079  tz7.49  8081  nneneq  8700  scottex  9314  dfac2b  9556  infpssrlem4  9728  fin23lem30  9764  fin23lem31  9765  hsmexlem2  9849  domtriomlem  9864  axdc3lem2  9873  axdc3lem4  9875  konigthlem  9990  winalim2  10118  nqereu  10351  dedekind  10803  dedekindle  10804  prodeq2ii  15267  vdwlem9  16325  mreiincl  16867  sgrpidmnd  17916  srgi  19261  ringi  19310  lbsextlem3  19932  lbsextlem4  19933  tgcl  21577  txindis  22242  alexsubALTlem3  22657  prdsxmslem2  23139  fsumcn  23478  lebnumlem1  23565  iscmet3lem1  23894  iscmet3lem2  23895  ovoliunlem2  24104  mbfimaopnlem  24256  limciun  24492  ftalem3  25652  ostth3  26214  mptelee  26681  ubthlem2  28648  aciunf1lem  30407  esumcvg  31345  bnj228  32005  bnj590  32182  bnj594  32184  bnj600  32191  bnj1128  32262  bnj1125  32264  bnj1145  32265  bnj1398  32306  bnj1417  32313  dfon2lem3  33030  dfon2lem7  33034  trpredmintr  33070  frr3g  33121  frrlem4  33126  frrlem8  33130  frrlem10  33132  frrlem13  33135  sslttr  33268  neibastop1  33707  unblimceq0lem  33845  unbdqndv2  33850  rdgssun  34662  ralssiun  34691  fvineqsneu  34695  fvineqsneq  34696  cover2  35004  upixp  35019  indexdom  35024  filbcmb  35030  mettrifi  35047  mpobi123f  35455  riotasvd  36107  glbconxN  36529  cdlemefr29exN  37553  cdlemk36  38064  mptfcl  39337  aomclem2  39675  hbtlem5  39748  gneispace  40504  trintALTVD  41234  trintALT  41235  refsumcn  41307  rfcnnnub  41313  choicefi  41483  mullimc  41917  mullimcf  41924  addlimc  41949  itgsubsticclem  42280  stoweidlem25  42330  stoweidlem52  42357  stoweidlem59  42364  stoweidlem62  42367  wallispilem3  42372  stirlinglem13  42391  fourierdlem73  42484  ffnafv  43390  iunord  44799  setrec1lem2  44811