Theorem rsp 2577

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1393   ∈ wcel 2200  ∀wral 2508

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

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

This theorem is referenced by:  rspa  2578  rsp2  2580  rspec  2582  r19.12  2637  ralbi  2663  rexbi  2664  reupick2  3490  dfiun2g  3997  iinss2  4018  invdisj  4076  mpteq12f  4164  trss  4191  sowlin  4411  reusv1  4549  reusv3  4551  ralxfrALT  4558  funimaexglem  5404  fun11iun  5595  fvmptssdm  5721  ffnfv  5795  riota5f  5987  mpoeq123  6069  tfri3  6519  nneneq  7026  mkvprop  7336  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemm  7866  suplocexprlemss  7913  suplocsrlem  8006  indstr  9800  nninfinf  10677  prodeq2  12083  fprodle  12166  bezoutlemzz  12538  sgrpidmndm  13468  srgdilem  13947  ringdilem  13990  tgcl  14753  fsumcncntop  15256  dedekindeulemlu  15310  dedekindicclemlu  15319  bj-rspgt  16205  bj-charfunr  16228