Theorem rsp 2589

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1396   ∈ wcel 2203  ∀wral 2520

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

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

This theorem is referenced by:  rspa  2590  rsp2  2592  rspec  2594  r19.12  2649  ralbi  2675  rexbi  2676  reupick2  3507  dfiun2g  4023  iinss2  4044  invdisj  4102  mpteq12f  4190  trss  4217  sowlin  4441  reusv1  4579  reusv3  4581  ralxfrALT  4588  funimaexglem  5439  fun11iun  5635  fvmptssdm  5762  ffnfv  5835  riota5f  6030  mpoeq123  6112  tfri3  6598  nneneq  7111  mkvprop  7449  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  caucvgprlemm  7983  suplocexprlemss  8030  suplocsrlem  8123  indstr  9925  nninfinf  10805  prodeq2  12243  fprodle  12326  bezoutlemzz  12698  sgrpidmndm  13633  srgdilem  14113  ringdilem  14156  tgcl  14929  fsumcncntop  15432  dedekindeulemlu  15486  dedekindicclemlu  15495  bj-rspgt  16558  bj-charfunr  16580