Theorem spcgv 2817

Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.)

Hypothesis

Ref	Expression
spcgv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
spcgv	⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem spcgv

Step	Hyp	Ref	Expression
1		nfcv 2312	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1521	. 2 ⊢ Ⅎ𝑥𝜓
3		spcgv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	1, 2, 3	spcgf 2812	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1346   = wceq 1348   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732

This theorem is referenced by:  spcv  2824  mob2  2910  intss1  3846  dfiin2g  3906  exmidsssnc  4189  frirrg  4335  frind  4337  alxfr  4446  elirr  4525  en2lp  4538  tfisi  4571  mptfvex  5581  tfrcl  6343  rdgisucinc  6364  frecabex  6377  fisseneq  6909  mkvprop  7134  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  acfun  7184  ccfunen  7226  zfz1isolem1  10775  zfz1iso  10776  uniopn  12793  exmid1stab  14033  pw1nct  14036  sbthom  14058