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  5998  mpoeq123  6080  tfri3  6533  nneneq  7043  mkvprop  7357  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemm  7888  suplocexprlemss  7935  suplocsrlem  8028  indstr  9827  nninfinf  10706  prodeq2  12123  fprodle  12206  bezoutlemzz  12578  sgrpidmndm  13508  srgdilem  13988  ringdilem  14031  tgcl  14794  fsumcncntop  15297  dedekindeulemlu  15351  dedekindicclemlu  15360  bj-rspgt  16408  bj-charfunr  16431