Theorem rsp 2544

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1362   ∈ wcel 2167  ∀wral 2475

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

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

This theorem is referenced by:  rspa  2545  rsp2  2547  rspec  2549  r19.12  2603  ralbi  2629  rexbi  2630  reupick2  3450  dfiun2g  3949  iinss2  3970  invdisj  4028  mpteq12f  4114  trss  4141  sowlin  4356  reusv1  4494  reusv3  4496  ralxfrALT  4503  funimaexglem  5342  fun11iun  5528  fvmptssdm  5649  ffnfv  5723  riota5f  5905  mpoeq123  5985  tfri3  6434  nneneq  6927  mkvprop  7233  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgprlemm  7754  suplocexprlemss  7801  suplocsrlem  7894  indstr  9686  nninfinf  10554  prodeq2  11741  fprodle  11824  bezoutlemzz  12196  sgrpidmndm  13124  srgdilem  13603  ringdilem  13646  tgcl  14408  fsumcncntop  14911  dedekindeulemlu  14965  dedekindicclemlu  14974  bj-rspgt  15540  bj-charfunr  15564