| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > spimevw | Structured version Visualization version GIF version | ||
| Description: Existential introduction, using implicit substitution. This is to spimew 1971 what spimvw 1995 is to spimw 1970. Version of spimev 2397 and spimefv 2198 with an additional disjoint variable condition, using only Tarski's FOL axiom schemes. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 17-Mar-2020.) |
| Ref | Expression |
|---|---|
| spimevw.1 | ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) |
| Ref | Expression |
|---|---|
| spimevw | ⊢ (𝜑 → ∃𝑥𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-5 1910 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
| 2 | spimevw.1 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) | |
| 3 | 1, 2 | spimew 1971 | 1 ⊢ (𝜑 → ∃𝑥𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: dtruALT2 5370 zfpair 5421 axprlem3 5425 exneq 5440 dtruOLD 5446 fvn0ssdmfun 7094 onsupmaxb 43251 refimssco 43620 rlimdmafv 47189 rlimdmafv2 47270 elsprel 47462 |
| Copyright terms: Public domain | W3C validator |