Theorem rsp 2580

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1396   ∈ wcel 2202  ∀wral 2511

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 2516

This theorem is referenced by:  rspa  2581  rsp2  2583  rspec  2585  r19.12  2640  ralbi  2666  rexbi  2667  reupick2  3495  dfiun2g  4007  iinss2  4028  invdisj  4086  mpteq12f  4174  trss  4201  sowlin  4423  reusv1  4561  reusv3  4563  ralxfrALT  4570  funimaexglem  5420  fun11iun  5613  fvmptssdm  5740  ffnfv  5813  riota5f  6008  mpoeq123  6090  tfri3  6576  nneneq  7086  mkvprop  7400  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemm  7931  suplocexprlemss  7978  suplocsrlem  8071  indstr  9871  nninfinf  10751  prodeq2  12181  fprodle  12264  bezoutlemzz  12636  sgrpidmndm  13566  srgdilem  14046  ringdilem  14089  tgcl  14858  fsumcncntop  15361  dedekindeulemlu  15415  dedekindicclemlu  15424  bj-rspgt  16487  bj-charfunr  16509