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  4212  trss  4240  sowlin  4467  reusv1  4606  reusv3  4608  ralxfrALT  4615  funimaexglem  5467  fun11iun  5663  fvmptssdm  5793  ffnfv  5869  riota5f  6068  mpoeq123  6150  tfri3  6642  nneneq  7162  mkvprop  7504  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemm  8041  suplocexprlemss  8088  suplocsrlem  8181  indstr  10009  nninfinf  10901  prodeq2  12349  fprodle  12432  bezoutlemzz  12804  sgrpidmndm  13792  srgdilem  14380  ringdilem  14423  tgcl  15290  fsumcncntop  15793  dedekindeulemlu  15847  dedekindicclemlu  15856  bj-rspgt  17019  bj-charfunr  17041