Theorem rsp 2597

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

Assertion

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

Proof of Theorem rsp

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1400   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-4 1563

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  rspa  2598  rsp2  2600  rspec  2602  r19.12  2657  ralbi  2683  rexbi  2684  reupick2  3519  dfiun2g  4044  iinss2  4065  invdisj  4123  mpteq12f  4211  trss  4238  sowlin  4465  reusv1  4604  reusv3  4606  ralxfrALT  4613  funimaexglem  5464  fun11iun  5660  fvmptssdm  5790  ffnfv  5866  riota5f  6065  mpoeq123  6147  tfri3  6638  nneneq  7158  mkvprop  7498  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemm  8035  suplocexprlemss  8082  suplocsrlem  8175  indstr  9993  nninfinf  10880  prodeq2  12324  fprodle  12407  bezoutlemzz  12779  sgrpidmndm  13733  srgdilem  14273  ringdilem  14316  tgcl  15165  fsumcncntop  15668  dedekindeulemlu  15722  dedekindicclemlu  15731  bj-rspgt  16814  bj-charfunr  16836