Theorem rsp 3129

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-ral 3068

This theorem is referenced by:  rspa  3130  rspec  3131  rsp2  3136  r19.12  3252  r19.12OLD  3253  2reu1  3826  reupick2  4251  rspn0OLD  4284  iuneqconst  4932  iinss2  4983  invdisj  5054  reusv1  5315  reusv2lem1  5316  reusv2lem3  5318  reusv3  5323  ralxfrALT  5333  fvmptss  6869  ffnfv  6974  riota5f  7241  mpoeq123  7325  peano5OLD  7715  frrlem4  8076  frrlem8  8080  frrlem10  8082  frrlem13  8085  wfrlem4OLD  8114  wfrlem12OLD  8122  tfr3  8201  tz7.48-1  8244  tz7.49  8246  nneneq  8896  trpredmintr  9409  frr3g  9445  scottex  9574  dfac2b  9817  infpssrlem4  9993  fin23lem30  10029  fin23lem31  10030  hsmexlem2  10114  domtriomlem  10129  axdc3lem2  10138  axdc3lem4  10140  konigthlem  10255  winalim2  10383  nqereu  10616  dedekind  11068  dedekindle  11069  prodeq2ii  15551  vdwlem9  16618  mreiincl  17222  sgrpidmnd  18305  srgi  19662  ringi  19714  lbsextlem3  20337  lbsextlem4  20338  tgcl  22027  txindis  22693  alexsubALTlem3  23108  prdsxmslem2  23591  fsumcn  23939  lebnumlem1  24030  iscmet3lem1  24360  iscmet3lem2  24361  ovoliunlem2  24572  mbfimaopnlem  24724  limciun  24963  ftalem3  26129  ostth3  26691  mptelee  27166  ubthlem2  29134  aciunf1lem  30901  esumcvg  31954  bnj228  32614  bnj590  32790  bnj594  32792  bnj600  32799  bnj1128  32870  bnj1125  32872  bnj1145  32873  bnj1398  32914  bnj1417  32921  dfon2lem3  33667  dfon2lem7  33671  neibastop1  34475  unblimceq0lem  34613  unbdqndv2  34618  rdgssun  35476  ralssiun  35505  fvineqsneu  35509  fvineqsneq  35510  cover2  35799  upixp  35814  indexdom  35819  filbcmb  35825  mettrifi  35842  mpobi123f  36247  riotasvd  36897  glbconxN  37319  cdlemefr29exN  38343  cdlemk36  38854  aks4d1p7d1  40018  mptfcl  40458  aomclem2  40796  hbtlem5  40869  gneispace  41633  trintALTVD  42389  trintALT  42390  refsumcn  42462  rfcnnnub  42468  choicefi  42629  mullimc  43047  mullimcf  43054  addlimc  43079  itgsubsticclem  43406  stoweidlem25  43456  stoweidlem52  43483  stoweidlem59  43490  stoweidlem62  43493  wallispilem3  43498  stirlinglem13  43517  fourierdlem73  43610  ffnafv  44550  iunord  46268  setrec1lem2  46280