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 2195 ax6e 2394 exdistrf 2464 equvini 2472 equviniOLD 2473 2ax6eOLD 2490 sb1OLD 2503 sbequ1OLD 2516 sbequ1ALT 2575 euor2 2693 2moexv 2708 2moswapv 2710 2euexv 2712 2moex 2721 2euex 2722 2moswap 2725 2mo 2729 rspe 3304 ceqex 3644 mo2icl 3704 intab 4899 eusv2nf 5287 copsexgw 5373 copsexg 5374 dmcosseq 5838 dminss 6004 imainss 6005 relssdmrn 6115 oprabidw 7176 oprabid 7177 hta 9315 axextnd 10002 axpowndlem2 10009 axregndlem1 10013 axregnd 10015 fpwwe 10057 reclem2pr 10459 bnj1121 32155 frrlem8 33028 frrlem10 33030 finminlem 33564 amosym1 33672 bj-19.23bit 33923 bj-nexrt 33924 bj-19.9htbi 33935 bj-sbsb 34058 bj-finsumval0 34456 wl-exeq 34656 ax12indn 35961 pm11.58 40602 axc11next 40618 iotavalsb 40645 vk15.4j 40742 onfrALTlem1 40762 onfrALTlem1VD 41104 vk15.4jVD 41128 suprnmpt 41310 ssfiunibd 41456 |
Copyright terms: Public domain | W3C validator |