Theorem rsp 2578

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1395   ∈ wcel 2201  ∀wral 2509

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

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

This theorem is referenced by:  rspa  2579  rsp2  2581  rspec  2583  r19.12  2638  ralbi  2664  rexbi  2665  reupick2  3492  dfiun2g  4001  iinss2  4022  invdisj  4080  mpteq12f  4168  trss  4195  sowlin  4416  reusv1  4554  reusv3  4556  ralxfrALT  4563  funimaexglem  5412  fun11iun  5604  fvmptssdm  5731  ffnfv  5805  riota5f  6000  mpoeq123  6082  tfri3  6535  nneneq  7045  mkvprop  7359  cauappcvgprlemladdru  7878  cauappcvgprlemladdrl  7879  caucvgprlemm  7890  suplocexprlemss  7937  suplocsrlem  8030  indstr  9829  nninfinf  10708  prodeq2  12138  fprodle  12221  bezoutlemzz  12593  sgrpidmndm  13523  srgdilem  14003  ringdilem  14046  tgcl  14814  fsumcncntop  15317  dedekindeulemlu  15371  dedekindicclemlu  15380  bj-rspgt  16440  bj-charfunr  16463