MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  spcv Structured version   Visualization version   GIF version

Theorem spcv 3268
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
StepHypRef Expression
1 spcv.1 . 2 𝐴 ∈ V
2 spcv.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32spcgv 3262 . 2 (𝐴 ∈ V → (∀𝑥𝜑𝜓))
41, 3ax-mp 5 1 (∀𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wal 1472   = wceq 1474  wcel 1976  Vcvv 3169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-v 3171
This theorem is referenced by:  morex  3353  rext  4834  relop  5179  frxp  7148  pssnn  8037  findcard  8058  fiint  8096  marypha1lem  8196  dfom3  8401  elom3  8402  aceq3lem  8800  dfac3  8801  dfac5lem4  8806  dfac8  8814  dfac9  8815  dfacacn  8820  dfac13  8821  kmlem1  8829  kmlem10  8838  fin23lem34  9025  fin23lem35  9026  zorn2lem7  9181  zornn0g  9184  axgroth6  9503  nnunb  11132  symggen  17656  gsumval3lem2  18073  gsumzaddlem  18087  dfac14  21170  i1fd  23168  chlimi  27278  ddemeas  29429  dfpo2  30701  dfon2lem4  30738  dfon2lem5  30739  dfon2lem7  30741  ttac  36421  dfac11  36450  dfac21  36454
  Copyright terms: Public domain W3C validator