Theorem rsp 2541

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1362   ∈ wcel 2164  ∀wral 2472

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

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

This theorem is referenced by:  rspa  2542  rsp2  2544  rspec  2546  r19.12  2600  ralbi  2626  rexbi  2627  reupick2  3446  dfiun2g  3945  iinss2  3966  invdisj  4024  mpteq12f  4110  trss  4137  sowlin  4352  reusv1  4490  reusv3  4492  ralxfrALT  4499  funimaexglem  5338  fun11iun  5522  fvmptssdm  5643  ffnfv  5717  riota5f  5899  mpoeq123  5978  tfri3  6422  nneneq  6915  mkvprop  7219  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  caucvgprlemm  7730  suplocexprlemss  7777  suplocsrlem  7870  indstr  9661  nninfinf  10517  prodeq2  11703  fprodle  11786  bezoutlemzz  12142  sgrpidmndm  13004  srgdilem  13468  ringdilem  13511  tgcl  14243  fsumcncntop  14746  dedekindeulemlu  14800  dedekindicclemlu  14809  bj-rspgt  15348  bj-charfunr  15372