Theorem spcgv 3548

Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.) Avoid ax-10 2146, ax-11 2162. (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 3459	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		id 22	. . 3 ⊢ (𝐴 ∈ V → 𝐴 ∈ V)
3		spcgv.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	adantl 481	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
5	2, 4	spcdv 3546	. 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓))
6	1, 5	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   = wceq 1541   ∈ wcel 2113  Vcvv 3438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440

This theorem is referenced by:  spcv  3557  mob2  3671  sbceqal  3800  intss1  4916  dfiin2g  4984  alxfr  5350  funmo  6506  isofrlem  7284  tfisi  7799  limomss  7811  nnlim  7820  f1oweALT  7914  pssnn  9091  findcard3  9181  frmin  9659  ttukeylem1  10417  rami  16941  ramcl  16955  islbs3  21108  mplsubglem  21952  mpllsslem  21953  uniopn  22839  chlimi  31258  iinabrex  32593  dfon2lem3  35926  dfon2lem8  35931  neificl  37893  hashnexinj  42321  ismrcd1  42882  mnuop23d  44449  relpfrlem  45136  modelaxreplem2  45162