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  3422  dfiun2g  3919  iinss2  3940  invdisj  3998  mpteq12f  4084  trss  4111  sowlin  4321  reusv1  4459  reusv3  4461  ralxfrALT  4468  funimaexglem  5300  fun11iun  5483  fvmptssdm  5601  ffnfv  5675  riota5f  5855  mpoeq123  5934  tfri3  6368  nneneq  6857  mkvprop  7156  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  caucvgprlemm  7667  suplocexprlemss  7714  suplocsrlem  7807  indstr  9593  prodeq2  11565  fprodle  11648  bezoutlemzz  12003  sgrpidmndm  12821  srgdilem  13152  ringdilem  13195  tgcl  13567  fsumcncntop  14059  dedekindeulemlu  14102  dedekindicclemlu  14111  bj-rspgt  14541  bj-charfunr  14565