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

Theorem spcimedv 3261
Description: Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
spcimdv.1 (𝜑𝐴𝐵)
spcimedv.2 ((𝜑𝑥 = 𝐴) → (𝜒𝜓))
Assertion
Ref Expression
spcimedv (𝜑 → (𝜒 → ∃𝑥𝜓))
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐵(𝑥)

Proof of Theorem spcimedv
StepHypRef Expression
1 spcimdv.1 . . . 4 (𝜑𝐴𝐵)
2 spcimedv.2 . . . . 5 ((𝜑𝑥 = 𝐴) → (𝜒𝜓))
32con3d 146 . . . 4 ((𝜑𝑥 = 𝐴) → (¬ 𝜓 → ¬ 𝜒))
41, 3spcimdv 3259 . . 3 (𝜑 → (∀𝑥 ¬ 𝜓 → ¬ 𝜒))
54con2d 127 . 2 (𝜑 → (𝜒 → ¬ ∀𝑥 ¬ 𝜓))
6 df-ex 1695 . 2 (∃𝑥𝜓 ↔ ¬ ∀𝑥 ¬ 𝜓)
75, 6syl6ibr 240 1 (𝜑 → (𝜒 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  wal 1472   = wceq 1474  wex 1694  wcel 1976
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:  hashf1rn  12953  hashf1rnOLD  12954  cshwsexa  13364  wwlktovfo  13492  uvcendim  19944  wlkiswwlk2  25988  wlknwwlknsur  26003  wlkiswwlksur  26010  wwlkextsur  26022  clwlkisclwwlklem2  26077  rtrclex  36743  clcnvlem  36749  iunrelexpuztr  36830  1wlkiswwlks2  41071  wlknwwlksnsur  41086  wlkwwlksur  41093  wwlksnextsur  41105  elwwlks2  41169  elwspths2spth  41170  clwlkclwwlklem1  41207
  Copyright terms: Public domain W3C validator