Theorem rsp 2483

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1330   ∈ wcel 1481  ∀wral 2417

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

This theorem depends on definitions:  df-bi 116  df-ral 2422

This theorem is referenced by:  rsp2  2485  rspec  2487  r19.12  2541  ralbi  2567  rexbi  2568  reupick2  3367  dfiun2g  3853  iinss2  3873  invdisj  3931  mpteq12f  4016  trss  4043  sowlin  4250  reusv1  4387  reusv3  4389  ralxfrALT  4396  funimaexglem  5214  fun11iun  5396  fvmptssdm  5513  ffnfv  5586  riota5f  5762  mpoeq123  5838  tfri3  6272  nneneq  6759  mkvprop  7040  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  caucvgprlemm  7500  suplocexprlemss  7547  suplocsrlem  7640  indstr  9415  prodeq2  11358  bezoutlemzz  11726  tgcl  12272  fsumcncntop  12764  dedekindeulemlu  12807  dedekindicclemlu  12816  bj-rspgt  13164