Theorem spcgv 3582

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1532   = wceq 1534   ∈ wcel 2099  Vcvv 3470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472

This theorem is referenced by:  spcv  3591  mob2  3709  sbceqal  3840  intss1  4962  dfiin2g  5030  alxfr  5402  friOLD  5634  funmo  6563  isofrlem  7343  tfisi  7858  limomss  7870  nnlim  7879  f1oweALT  7971  pssnn  9187  pssnnOLD  9284  findcard3  9304  findcard3OLD  9305  frmin  9767  ttukeylem1  10527  rami  16978  ramcl  16992  islbs3  21037  mplsubglem  21935  mpllsslem  21936  uniopn  22793  chlimi  31038  iinabrex  32353  dfon2lem3  35376  dfon2lem8  35381  neificl  37221  hashnexinj  41594  ismrcd1  42109  mnuop23d  43694