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 1882 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2041. (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 2035 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | |
2 | ax6ev 1877 | . . 3 ⊢ ∃𝑥 𝑥 = 𝑦 | |
3 | exim 1751 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥𝜑)) | |
4 | 1, 2, 3 | syl6mpi 65 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑)) |
5 | ax6evr 1929 | . 2 ⊢ ∃𝑦 𝑥 = 𝑦 | |
6 | 4, 5 | exlimiiv 1846 | 1 ⊢ (𝜑 → ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1473 ∃wex 1695 |
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-12 2034 |
This theorem depends on definitions: df-bi 196 df-ex 1696 |
This theorem is referenced by: sp 2041 19.2g 2046 19.23bi 2049 nexr 2050 qexmid 2051 nf5r 2052 19.9t 2059 sbequ1 2096 19.9tOLD 2192 ax6e 2238 exdistrf 2321 equvini 2334 2ax6e 2438 euor2 2502 2moex 2531 2euex 2532 2moswap 2535 2mo 2539 rspe 2986 ceqex 3303 mo2icl 3352 intab 4442 eusv2nf 4790 copsexg 4882 dmcosseq 5308 dminss 5466 imainss 5467 relssdmrn 5573 oprabid 6576 hta 8643 domtriomlem 9147 axextnd 9292 axrepnd 9295 axunndlem1 9296 axunnd 9297 axpowndlem2 9299 axpownd 9302 axregndlem1 9303 axregnd 9305 axacndlem1 9308 axacndlem2 9309 axacndlem3 9310 axacndlem4 9311 axacndlem5 9312 axacnd 9313 fpwwe 9347 pwfseqlem4a 9362 pwfseqlem4 9363 reclem2pr 9749 bnj1121 30307 bnj1189 30331 finminlem 31482 amosym1 31595 bj-ssbft 31831 bj-19.23bit 31868 bj-nexrt 31869 bj-19.9htbi 31881 bj-sbsb 32012 bj-nfdiOLD 32019 bj-xnex 32245 bj-finsumval0 32324 isbasisrelowllem1 32379 isbasisrelowllem2 32380 wl-exeq 32500 ax12indn 33246 gneispace 37452 pm11.58 37612 axc11next 37629 iotavalsb 37656 vk15.4j 37755 onfrALTlem1 37784 onfrALTlem1VD 38148 vk15.4jVD 38172 suprnmpt 38350 ssfiunibd 38464 ovncvrrp 39454 19.8ad 42257 |
Copyright terms: Public domain | W3C validator |