New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  spcev GIF version

Theorem spcev 2946
 Description: Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
Hypotheses
Ref Expression
spcv.1 A V
spcv.2 (x = A → (φψ))
Assertion
Ref Expression
spcev (ψxφ)
Distinct variable groups:   x,A   ψ,x
Allowed substitution hint:   φ(x)

Proof of Theorem spcev
StepHypRef Expression
1 spcv.1 . 2 A V
2 spcv.2 . . 3 (x = A → (φψ))
32spcegv 2940 . 2 (A V → (ψxφ))
41, 3ax-mp 8 1 (ψxφ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2859 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861 This theorem is referenced by:  snel1c  4140  sspw1  4335  sspw12  4336  sfin01  4528  sfindbl  4530  1cvsfin  4542  vfinspsslem1  4550  phialllem1  4616  phialllem2  4617  nfunv  5138  ffoss  5314  map0  6025  unen  6048  enpw1  6062  1cnc  6139  ncaddccl  6144  ce0addcnnul  6179  ce0nulnc  6184  dflec3  6221  nclenc  6222
 Copyright terms: Public domain W3C validator