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 1978 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2172. (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 2168 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | |
2 | alequexv 1998 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑) | |
3 | 1, 2 | syl6 35 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑)) |
4 | ax6evr 2013 | . 2 ⊢ ∃𝑦 𝑥 = 𝑦 | |
5 | 3, 4 | exlimiiv 1923 | 1 ⊢ (𝜑 → ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-ex 1772 |
This theorem is referenced by: 19.8ad 2171 sp 2172 19.2g 2177 19.23bi 2180 nexr 2181 qexmid 2182 nf5r 2183 nf5rOLD 2184 19.9t 2194 ax6e 2392 exdistrf 2461 equvini 2469 equviniOLD 2470 2ax6eOLD 2487 sb1OLD 2500 sbequ1OLD 2513 sbequ1ALT 2572 euor2 2690 2moexv 2705 2moswapv 2707 2euexv 2709 2moex 2718 2euex 2719 2moswap 2722 2mo 2726 rspe 3301 ceqex 3642 mo2icl 3702 intab 4897 eusv2nf 5286 copsexgw 5372 copsexg 5373 dmcosseq 5837 dminss 6003 imainss 6004 relssdmrn 6114 oprabidw 7176 oprabid 7177 hta 9314 axextnd 10001 axpowndlem2 10008 axregndlem1 10012 axregnd 10014 fpwwe 10056 reclem2pr 10458 bnj1121 32154 frrlem8 33027 frrlem10 33029 finminlem 33563 amosym1 33671 bj-19.23bit 33922 bj-nexrt 33923 bj-19.9htbi 33934 bj-sbsb 34057 bj-finsumval0 34455 wl-exeq 34655 ax12indn 35959 pm11.58 40599 axc11next 40615 iotavalsb 40642 vk15.4j 40739 onfrALTlem1 40759 onfrALTlem1VD 41101 vk15.4jVD 41125 suprnmpt 41306 ssfiunibd 41452 |
Copyright terms: Public domain | W3C validator |