Theorem rsp 2517

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1346   ∈ wcel 2141  ∀wral 2448

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

This theorem depends on definitions:  df-bi 116  df-ral 2453

This theorem is referenced by:  rspa  2518  rsp2  2520  rspec  2522  r19.12  2576  ralbi  2602  rexbi  2603  reupick2  3413  dfiun2g  3905  iinss2  3925  invdisj  3983  mpteq12f  4069  trss  4096  sowlin  4305  reusv1  4443  reusv3  4445  ralxfrALT  4452  funimaexglem  5281  fun11iun  5463  fvmptssdm  5580  ffnfv  5654  riota5f  5833  mpoeq123  5912  tfri3  6346  nneneq  6835  mkvprop  7134  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgprlemm  7630  suplocexprlemss  7677  suplocsrlem  7770  indstr  9552  prodeq2  11520  fprodle  11603  bezoutlemzz  11957  sgrpidmndm  12656  tgcl  12858  fsumcncntop  13350  dedekindeulemlu  13393  dedekindicclemlu  13402  bj-rspgt  13821  bj-charfunr  13845