Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > spcimedv | Structured version Visualization version GIF version |
Description: Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Ref | Expression |
---|---|
spcimdv.1 | ⊢ (𝜑 → 𝐴 ∈ 𝐵) |
spcimedv.2 | ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) |
Ref | Expression |
---|---|
spcimedv | ⊢ (𝜑 → (𝜒 → ∃𝑥𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spcimdv.1 | . . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝐵) | |
2 | spcimedv.2 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) | |
3 | 2 | con3d 147 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (¬ 𝜓 → ¬ 𝜒)) |
4 | 1, 3 | spcimdv 3263 | . . 3 ⊢ (𝜑 → (∀𝑥 ¬ 𝜓 → ¬ 𝜒)) |
5 | 4 | con2d 128 | . 2 ⊢ (𝜑 → (𝜒 → ¬ ∀𝑥 ¬ 𝜓)) |
6 | df-ex 1696 | . 2 ⊢ (∃𝑥𝜓 ↔ ¬ ∀𝑥 ¬ 𝜓) | |
7 | 5, 6 | syl6ibr 241 | 1 ⊢ (𝜑 → (𝜒 → ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 ∀wal 1473 = wceq 1475 ∃wex 1695 ∈ wcel 1977 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 |
This theorem is referenced by: hashf1rn 13004 hashf1rnOLD 13005 cshwsexa 13421 wwlktovfo 13549 uvcendim 20005 wlkiswwlk2 26225 wlknwwlknsur 26240 wlkiswwlksur 26247 wwlkextsur 26259 clwlkisclwwlklem2 26314 rtrclex 36943 clcnvlem 36949 iunrelexpuztr 37030 1wlkiswwlks2 41072 wlknwwlksnsur 41087 wlkwwlksur 41094 wwlksnextsur 41106 elwwlks2 41170 elwspths2spth 41171 clwlkclwwlklem1 41208 |
Copyright terms: Public domain | W3C validator |