Theorem rsp 2544

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1362   ∈ wcel 2167  ∀wral 2475

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

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

This theorem is referenced by:  rspa  2545  rsp2  2547  rspec  2549  r19.12  2603  ralbi  2629  rexbi  2630  reupick2  3449  dfiun2g  3948  iinss2  3969  invdisj  4027  mpteq12f  4113  trss  4140  sowlin  4355  reusv1  4493  reusv3  4495  ralxfrALT  4502  funimaexglem  5341  fun11iun  5525  fvmptssdm  5646  ffnfv  5720  riota5f  5902  mpoeq123  5981  tfri3  6425  nneneq  6918  mkvprop  7224  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgprlemm  7735  suplocexprlemss  7782  suplocsrlem  7875  indstr  9667  nninfinf  10535  prodeq2  11722  fprodle  11805  bezoutlemzz  12169  sgrpidmndm  13061  srgdilem  13525  ringdilem  13568  tgcl  14300  fsumcncntop  14803  dedekindeulemlu  14857  dedekindicclemlu  14866  bj-rspgt  15432  bj-charfunr  15456