Theorem spcv 3544

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 3535	. 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539   ∈ wcel 2106  Vcvv 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434

This theorem is referenced by:  morex  3654  al0ssb  5232  rext  5364  relop  5759  dfpo2  6199  frxp  7967  findcard  8946  pssnn  8951  ssfi  8956  pssnnOLD  9040  fiint  9091  marypha1lem  9192  dfom3  9405  elom3  9406  ttrclss  9478  aceq3lem  9876  dfac3  9877  dfac5lem4  9882  dfac8  9891  dfac9  9892  dfacacn  9897  dfac13  9898  kmlem1  9906  kmlem10  9915  fin23lem34  10102  fin23lem35  10103  zorn2lem7  10258  zornn0g  10261  axgroth6  10584  nnunb  12229  symggen  19078  gsumval3lem2  19507  gsumzaddlem  19522  dfac14  22769  i1fd  24845  chlimi  29596  zarclssn  31823  ddemeas  32204  dfon2lem4  33762  dfon2lem5  33763  dfon2lem7  33765  frxp2  33791  frxp3  33797  ttac  40858  dfac11  40887  dfac21  40891  setrec2fun  46398