Theorem rsp 2552

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1370   ∈ wcel 2175  ∀wral 2483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-4 1532

This theorem depends on definitions:  df-bi 117  df-ral 2488

This theorem is referenced by:  rspa  2553  rsp2  2555  rspec  2557  r19.12  2611  ralbi  2637  rexbi  2638  reupick2  3458  dfiun2g  3958  iinss2  3979  invdisj  4037  mpteq12f  4123  trss  4150  sowlin  4366  reusv1  4504  reusv3  4506  ralxfrALT  4513  funimaexglem  5356  fun11iun  5542  fvmptssdm  5663  ffnfv  5737  riota5f  5923  mpoeq123  6003  tfri3  6452  nneneq  6953  mkvprop  7259  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  caucvgprlemm  7780  suplocexprlemss  7827  suplocsrlem  7920  indstr  9713  nninfinf  10586  prodeq2  11839  fprodle  11922  bezoutlemzz  12294  sgrpidmndm  13223  srgdilem  13702  ringdilem  13745  tgcl  14507  fsumcncntop  15010  dedekindeulemlu  15064  dedekindicclemlu  15073  bj-rspgt  15684  bj-charfunr  15708