Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  spcev GIF version

Theorem spcev 2662
 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 𝐴 ∈ V
spcv.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
spcev (𝜓 → ∃𝑥𝜑)
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem spcev
StepHypRef Expression
1 spcv.1 . 2 𝐴 ∈ V
2 spcv.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32spcegv 2656 . 2 (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
41, 3ax-mp 7 1 (𝜓 → ∃𝑥𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102   = wceq 1257  ∃wex 1395   ∈ wcel 1407  Vcvv 2572 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036 This theorem depends on definitions:  df-bi 114  df-tru 1260  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-v 2574 This theorem is referenced by:  bnd2  3951  mss  3987  exss  3988  snnex  4206  opeldm  4563  elrnmpt1  4610  xpmlem  4769  ffoss  5183  ssimaex  5259  fvelrn  5323  eufnfv  5414  foeqcnvco  5455  cnvoprab  5880  domtr  6293  ensn1  6304  ac6sfi  6380
 Copyright terms: Public domain W3C validator