Theorem rsp 2480

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1329   ∈ wcel 1480  ∀wral 2416

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

This theorem depends on definitions:  df-bi 116  df-ral 2421

This theorem is referenced by:  rsp2  2482  rspec  2484  r19.12  2538  ralbi  2564  rexbi  2565  reupick2  3362  dfiun2g  3845  iinss2  3865  invdisj  3923  mpteq12f  4008  trss  4035  sowlin  4242  reusv1  4379  reusv3  4381  ralxfrALT  4388  funimaexglem  5206  fun11iun  5388  fvmptssdm  5505  ffnfv  5578  riota5f  5754  mpoeq123  5830  tfri3  6264  nneneq  6751  mkvprop  7032  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgprlemm  7476  suplocexprlemss  7523  suplocsrlem  7616  indstr  9388  prodeq2  11326  bezoutlemzz  11690  tgcl  12233  fsumcncntop  12725  dedekindeulemlu  12768  dedekindicclemlu  12777  bj-rspgt  12993