Theorem spcgv 3562

Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.) Avoid ax-10 2142, ax-11 2158. (Revised by Wolf Lammen, 25-Aug-2023.)

Hypothesis

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

Assertion

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

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

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

Proof of Theorem spcgv

Step	Hyp	Ref	Expression
1		elex 3468	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		id 22	. . 3 ⊢ (𝐴 ∈ V → 𝐴 ∈ V)
3		spcgv.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	adantl 481	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
5	2, 4	spcdv 3560	. 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓))
6	1, 5	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540   ∈ wcel 2109  Vcvv 3447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449

This theorem is referenced by:  spcv  3571  mob2  3686  sbceqal  3815  intss1  4927  dfiin2g  4996  alxfr  5362  funmo  6531  isofrlem  7315  tfisi  7835  limomss  7847  nnlim  7856  f1oweALT  7951  pssnn  9132  findcard3  9229  findcard3OLD  9230  frmin  9702  ttukeylem1  10462  rami  16986  ramcl  17000  islbs3  21065  mplsubglem  21908  mpllsslem  21909  uniopn  22784  chlimi  31163  iinabrex  32498  dfon2lem3  35773  dfon2lem8  35778  neificl  37747  hashnexinj  42116  ismrcd1  42686  mnuop23d  44255  relpfrlem  44943  modelaxreplem2  44969