Theorem rsp 2554

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1371   ∈ wcel 2177  ∀wral 2485

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

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

This theorem is referenced by:  rspa  2555  rsp2  2557  rspec  2559  r19.12  2613  ralbi  2639  rexbi  2640  reupick2  3463  dfiun2g  3965  iinss2  3986  invdisj  4044  mpteq12f  4132  trss  4159  sowlin  4375  reusv1  4513  reusv3  4515  ralxfrALT  4522  funimaexglem  5366  fun11iun  5555  fvmptssdm  5677  ffnfv  5751  riota5f  5937  mpoeq123  6017  tfri3  6466  nneneq  6969  mkvprop  7275  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  caucvgprlemm  7801  suplocexprlemss  7848  suplocsrlem  7941  indstr  9734  nninfinf  10610  prodeq2  11943  fprodle  12026  bezoutlemzz  12398  sgrpidmndm  13327  srgdilem  13806  ringdilem  13849  tgcl  14611  fsumcncntop  15114  dedekindeulemlu  15168  dedekindicclemlu  15177  bj-rspgt  15861  bj-charfunr  15884