![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ax6ev | Structured version Visualization version GIF version |
Description: At least one individual exists. Weaker version of ax6e 2387. When possible, use of this theorem rather than ax6e 2387 is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 3-Aug-2017.) |
Ref | Expression |
---|---|
ax6ev | ⊢ ∃𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax6v 2047 | . 2 ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | |
2 | df-ex 1846 | . 2 ⊢ (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦) | |
3 | 1, 2 | mpbir 221 | 1 ⊢ ∃𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1622 ∃wex 1845 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-6 2046 |
This theorem depends on definitions: df-bi 197 df-ex 1846 |
This theorem is referenced by: exiftru 2049 spimeh 2072 equs4v 2077 equsalvw 2078 equsexvw 2079 equid 2086 ax6evr 2089 equvinv 2104 aeveq 2125 19.8a 2191 equsalv 2247 equsexv 2248 spimv1 2254 equsalhw 2262 ax6e 2387 axc15 2440 axc11nOLD 2444 sbcom2 2574 euex 2623 axext3 2734 dfdif3 3855 dmi 5487 snnexOLD 7124 1st2val 7353 2nd2val 7354 bnj1468 31215 bj-sbex 32924 bj-ssbeq 32925 bj-ssb0 32926 bj-ssb1 32931 bj-equsexval 32936 bj-ssbid2ALT 32944 bj-ax6elem2 32950 bj-alequexv 32953 bj-eqs 32961 bj-spimtv 33016 bj-spimedv 33017 bj-spimvv 33019 bj-speiv 33022 bj-dtrucor2v 33099 bj-cleljustab 33145 wl-sbcom2d 33649 wl-euequ1f 33661 axc11n-16 34719 ax12eq 34722 ax12el 34723 ax12inda 34729 ax12v2-o 34730 relexp0eq 38487 ax6e2eq 39267 relopabVD 39628 ax6e2eqVD 39634 |
Copyright terms: Public domain | W3C validator |