![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 19.8a | Structured version Visualization version GIF version |
Description: If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. See 19.8v 1986 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2176. (Revised by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 8-Dec-2019.) |
Ref | Expression |
---|---|
19.8a | ⊢ (𝜑 → ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax12v 2172 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | |
2 | alequexv 2004 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑) | |
3 | 1, 2 | syl6 35 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑)) |
4 | ax6evr 2018 | . 2 ⊢ ∃𝑦 𝑥 = 𝑦 | |
5 | 3, 4 | exlimiiv 1934 | 1 ⊢ (𝜑 → ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1539 ∃wex 1781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-12 2171 |
This theorem depends on definitions: df-bi 206 df-ex 1782 |
This theorem is referenced by: 19.8ad 2175 sp 2176 19.2g 2181 19.23bi 2184 nexr 2185 qexmid 2186 nf5r 2187 19.9t 2197 ax6e 2381 exdistrf 2445 equvini 2453 euor2 2608 2moexv 2622 2moswapv 2624 2euexv 2626 2moex 2635 2euex 2636 2moswap 2639 2mo 2643 rspe 3245 ceqex 3636 intab 4975 eusv2nf 5386 copsexgw 5483 copsexg 5484 dmcosseq 5964 dminss 6141 imainss 6142 relssdmrnOLD 6257 oprabidw 7424 oprabid 7425 frrlem8 8260 frrlem10 8262 hta 9874 axextnd 10568 axpowndlem2 10575 axregndlem1 10579 axregnd 10581 fpwwe 10623 reclem2pr 11025 bnj1121 33825 finminlem 35005 bj-19.23bit 35371 bj-nexrt 35372 bj-19.9htbi 35383 bj-sbsb 35517 bj-finsumval0 35968 wl-exeq 36205 mopickr 37035 ax12indn 37616 pm11.58 42918 axc11next 42934 iotavalsb 42961 vk15.4j 43058 onfrALTlem1 43078 onfrALTlem1VD 43420 vk15.4jVD 43444 suprnmpt 43639 ssfiunibd 43790 pgind 47408 |
Copyright terms: Public domain | W3C validator |