Theorem rsp 2579

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1395   ∈ wcel 2202  ∀wral 2510

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

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

This theorem is referenced by:  rspa  2580  rsp2  2582  rspec  2584  r19.12  2639  ralbi  2665  rexbi  2666  reupick2  3493  dfiun2g  4002  iinss2  4023  invdisj  4081  mpteq12f  4169  trss  4196  sowlin  4417  reusv1  4555  reusv3  4557  ralxfrALT  4564  funimaexglem  5413  fun11iun  5604  fvmptssdm  5731  ffnfv  5805  riota5f  5997  mpoeq123  6079  tfri3  6532  nneneq  7042  mkvprop  7356  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgprlemm  7887  suplocexprlemss  7934  suplocsrlem  8027  indstr  9826  nninfinf  10704  prodeq2  12117  fprodle  12200  bezoutlemzz  12572  sgrpidmndm  13502  srgdilem  13981  ringdilem  14024  tgcl  14787  fsumcncntop  15290  dedekindeulemlu  15344  dedekindicclemlu  15353  bj-rspgt  16382  bj-charfunr  16405