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

Theorem spcv 3289
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 3283 . 2 (𝐴 ∈ V → (∀𝑥𝜑𝜓))
41, 3ax-mp 5 1 (∀𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1478   = wceq 1480  wcel 1987  Vcvv 3190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192
This theorem is referenced by:  morex  3377  rext  4887  relop  5242  frxp  7247  pssnn  8138  findcard  8159  fiint  8197  marypha1lem  8299  dfom3  8504  elom3  8505  aceq3lem  8903  dfac3  8904  dfac5lem4  8909  dfac8  8917  dfac9  8918  dfacacn  8923  dfac13  8924  kmlem1  8932  kmlem10  8941  fin23lem34  9128  fin23lem35  9129  zorn2lem7  9284  zornn0g  9287  axgroth6  9610  nnunb  11248  symggen  17830  gsumval3lem2  18247  gsumzaddlem  18261  dfac14  21361  i1fd  23388  chlimi  27979  ddemeas  30122  dfpo2  31406  dfon2lem4  31445  dfon2lem5  31446  dfon2lem7  31448  ttac  37122  dfac11  37151  dfac21  37155  setrec2fun  41762
  Copyright terms: Public domain W3C validator