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  3491  dfiun2g  4000  iinss2  4021  invdisj  4079  mpteq12f  4167  trss  4194  sowlin  4415  reusv1  4553  reusv3  4555  ralxfrALT  4562  funimaexglem  5410  fun11iun  5601  fvmptssdm  5727  ffnfv  5801  riota5f  5993  mpoeq123  6075  tfri3  6528  nneneq  7038  mkvprop  7348  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgprlemm  7878  suplocexprlemss  7925  suplocsrlem  8018  indstr  9817  nninfinf  10695  prodeq2  12108  fprodle  12191  bezoutlemzz  12563  sgrpidmndm  13493  srgdilem  13972  ringdilem  14015  tgcl  14778  fsumcncntop  15281  dedekindeulemlu  15335  dedekindicclemlu  15344  bj-rspgt  16318  bj-charfunr  16341