Theorem spcgv 3266

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

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175

This theorem is referenced by:  spcv  3272  mob2  3353  intss1  4427  dfiin2g  4489  alxfr  4804  fri  5000  isofrlem  6490  tfisi  6950  limomss  6962  nnlim  6970  f1oweALT  7043  pssnn  8063  findcard3  8088  ttukeylem1  9214  rami  15557  ramcl  15571  islbs3  18976  mplsubglem  19255  mpllsslem  19256  uniopn  20527  0eusgraiff0rgra  26466  chlimi  27475  dfon2lem3  30934  dfon2lem8  30939  neificl  32719  ismrcd1  36279