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 3483	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		id 22	. . 3 ⊢ (𝐴 ∈ V → 𝐴 ∈ V)
3		spcgv.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	adantl 480	. . 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 3463

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 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3465

This theorem is referenced by:  spcv  3591  mob2  3709  sbceqal  3842  intss1  4964  dfiin2g  5033  alxfr  5402  friOLD  5634  funmo  6564  isofrlem  7342  tfisi  7859  limomss  7871  nnlim  7880  f1oweALT  7976  pssnn  9196  pssnnOLD  9290  findcard3  9310  findcard3OLD  9311  frmin  9783  ttukeylem1  10541  rami  17010  ramcl  17024  islbs3  21130  mplsubglem  22002  mpllsslem  22003  uniopn  22885  chlimi  31162  iinabrex  32487  dfon2lem3  35620  dfon2lem8  35625  neificl  37465  hashnexinj  41838  ismrcd1  42390  mnuop23d  43975