Theorem spcgv 3535

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1546   = wceq 1548   ∈ wcel 2121  Vcvv 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435

This theorem is referenced by:  spcv  3544  mob2  3657  sbceqal  3785  intss1  4895  alxfr  5338  funmo  6504  isofrlem  7287  tfisi  7802  limomss  7814  nnlim  7823  f1oweALT  7916  pssnn  9097  findcard3  9187  frmin  9668  ttukeylem1  10427  rami  16981  ramcl  16995  islbs3  21151  mplsubglem  21976  mpllsslem  21977  uniopn  22883  chlimi  31325  iinabrex  32660  dfon2lem3  36024  dfon2lem8  36029  neificl  38133  hashnexinj  42626  ismrcd1  43160  mnuop23d  44723  relpfrlem  45410  modelaxreplem2  45436