Theorem spcv 3272

Description: Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.)

Hypotheses

Ref	Expression
spcv.1	⊢ 𝐴 ∈ V
spcv.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
spcv	⊢ (∀𝑥𝜑 → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem spcv

Step	Hyp	Ref	Expression
1		spcv.1	. 2 ⊢ 𝐴 ∈ V
2		spcv.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	spcgv 3266	. 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473   = wceq 1475   ∈ wcel 1977  Vcvv 3173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175

This theorem is referenced by:  morex  3357  rext  4843  relop  5194  frxp  7174  pssnn  8063  findcard  8084  fiint  8122  marypha1lem  8222  dfom3  8427  elom3  8428  aceq3lem  8826  dfac3  8827  dfac5lem4  8832  dfac8  8840  dfac9  8841  dfacacn  8846  dfac13  8847  kmlem1  8855  kmlem10  8864  fin23lem34  9051  fin23lem35  9052  zorn2lem7  9207  zornn0g  9210  axgroth6  9529  nnunb  11165  symggen  17713  gsumval3lem2  18130  gsumzaddlem  18144  dfac14  21231  i1fd  23254  chlimi  27475  ddemeas  29626  dfpo2  30898  dfon2lem4  30935  dfon2lem5  30936  dfon2lem7  30938  ttac  36621  dfac11  36650  dfac21  36654  setrec2fun  42238