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  3490  dfiun2g  3996  iinss2  4017  invdisj  4075  mpteq12f  4163  trss  4190  sowlin  4410  reusv1  4548  reusv3  4550  ralxfrALT  4557  funimaexglem  5403  fun11iun  5592  fvmptssdm  5718  ffnfv  5792  riota5f  5980  mpoeq123  6062  tfri3  6511  nneneq  7014  mkvprop  7321  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  caucvgprlemm  7851  suplocexprlemss  7898  suplocsrlem  7991  indstr  9784  nninfinf  10660  prodeq2  12063  fprodle  12146  bezoutlemzz  12518  sgrpidmndm  13448  srgdilem  13927  ringdilem  13970  tgcl  14732  fsumcncntop  15235  dedekindeulemlu  15289  dedekindicclemlu  15298  bj-rspgt  16108  bj-charfunr  16131