Theorem rsp 2524

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1351   ∈ wcel 2148  ∀wral 2455

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

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

This theorem is referenced by:  rspa  2525  rsp2  2527  rspec  2529  r19.12  2583  ralbi  2609  rexbi  2610  reupick2  3421  dfiun2g  3918  iinss2  3938  invdisj  3996  mpteq12f  4082  trss  4109  sowlin  4319  reusv1  4457  reusv3  4459  ralxfrALT  4466  funimaexglem  5298  fun11iun  5481  fvmptssdm  5599  ffnfv  5673  riota5f  5852  mpoeq123  5931  tfri3  6365  nneneq  6854  mkvprop  7153  cauappcvgprlemladdru  7652  cauappcvgprlemladdrl  7653  caucvgprlemm  7664  suplocexprlemss  7711  suplocsrlem  7804  indstr  9589  prodeq2  11558  fprodle  11641  bezoutlemzz  11995  sgrpidmndm  12753  srgdilem  13083  ringdilem  13126  tgcl  13435  fsumcncntop  13927  dedekindeulemlu  13970  dedekindicclemlu  13979  bj-rspgt  14398  bj-charfunr  14422