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  3445  dfiun2g  3944  iinss2  3965  invdisj  4023  mpteq12f  4109  trss  4136  sowlin  4351  reusv1  4489  reusv3  4491  ralxfrALT  4498  funimaexglem  5337  fun11iun  5521  fvmptssdm  5642  ffnfv  5716  riota5f  5898  mpoeq123  5977  tfri3  6420  nneneq  6913  mkvprop  7217  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  caucvgprlemm  7728  suplocexprlemss  7775  suplocsrlem  7868  indstr  9658  nninfinf  10514  prodeq2  11700  fprodle  11783  bezoutlemzz  12139  sgrpidmndm  13001  srgdilem  13465  ringdilem  13508  tgcl  14232  fsumcncntop  14724  dedekindeulemlu  14775  dedekindicclemlu  14784  bj-rspgt  15278  bj-charfunr  15302