Theorem spcgv 2860

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 2348	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1551	. 2 ⊢ Ⅎ𝑥𝜓
3		spcgv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	1, 2, 3	spcgf 2855	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1371   = wceq 1373   ∈ wcel 2176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774

This theorem is referenced by:  spcv  2867  mob2  2953  intss1  3900  dfiin2g  3960  exmidsssnc  4248  exmid1stab  4253  frirrg  4398  frind  4400  alxfr  4509  elirr  4590  en2lp  4603  tfisi  4636  mptfvex  5667  tfrcl  6452  rdgisucinc  6473  frecabex  6486  fisseneq  7033  mkvprop  7262  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  acfun  7321  exmidmotap  7375  ccfunen  7378  zfz1isolem1  10987  zfz1iso  10988  uniopn  14506  pw1nct  15977  sbthom  16002