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  4365  reusv1  4503  reusv3  4505  ralxfrALT  4512  funimaexglem  5351  fun11iun  5537  fvmptssdm  5658  ffnfv  5732  riota5f  5914  mpoeq123  5994  tfri3  6443  nneneq  6936  mkvprop  7242  cauappcvgprlemladdru  7751  cauappcvgprlemladdrl  7752  caucvgprlemm  7763  suplocexprlemss  7810  suplocsrlem  7903  indstr  9696  nninfinf  10569  prodeq2  11787  fprodle  11870  bezoutlemzz  12242  sgrpidmndm  13170  srgdilem  13649  ringdilem  13692  tgcl  14454  fsumcncntop  14957  dedekindeulemlu  15011  dedekindicclemlu  15020  bj-rspgt  15586  bj-charfunr  15610