Theorem spcgv 3539

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   = wceq 1542   ∈ wcel 2114  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432

This theorem is referenced by:  spcv  3548  mob2  3662  sbceqal  3791  intss1  4906  alxfr  5346  funmo  6510  isofrlem  7290  tfisi  7805  limomss  7817  nnlim  7826  f1oweALT  7920  pssnn  9098  findcard3  9188  frmin  9668  ttukeylem1  10426  rami  16981  ramcl  16995  islbs3  21149  mplsubglem  21991  mpllsslem  21992  uniopn  22876  chlimi  31324  iinabrex  32658  dfon2lem3  35985  dfon2lem8  35990  neificl  38092  hashnexinj  42585  ismrcd1  43148  mnuop23d  44715  relpfrlem  45402  modelaxreplem2  45428