Theorem rsp 2591

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1396   ∈ wcel 2205  ∀wral 2522

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

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

This theorem is referenced by:  rspa  2592  rsp2  2594  rspec  2596  r19.12  2651  ralbi  2677  rexbi  2678  reupick2  3511  dfiun2g  4028  iinss2  4049  invdisj  4107  mpteq12f  4195  trss  4222  sowlin  4446  reusv1  4584  reusv3  4586  ralxfrALT  4593  funimaexglem  5444  fun11iun  5640  fvmptssdm  5767  ffnfv  5840  riota5f  6038  mpoeq123  6120  tfri3  6611  nneneq  7124  mkvprop  7462  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemm  7999  suplocexprlemss  8046  suplocsrlem  8139  indstr  9943  nninfinf  10829  prodeq2  12268  fprodle  12351  bezoutlemzz  12723  sgrpidmndm  13681  srgdilem  14212  ringdilem  14255  tgcl  15055  fsumcncntop  15558  dedekindeulemlu  15612  dedekindicclemlu  15621  bj-rspgt  16684  bj-charfunr  16706