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 2238. When possible, use of this theorem rather than ax6e 2238 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 1876 | . 2 ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | |
2 | df-ex 1696 | . 2 ⊢ (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦) | |
3 | 1, 2 | mpbir 220 | 1 ⊢ ∃𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1473 ∃wex 1695 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-6 1875 |
This theorem depends on definitions: df-bi 196 df-ex 1696 |
This theorem is referenced by: exiftru 1878 spimeh 1912 equs4v 1917 equsalvw 1918 equsexvw 1919 equid 1926 ax6evr 1929 equvinv 1946 equvinivOLD 1948 aeveq 1969 ax12vOLDOLD 2038 19.8a 2039 19.8aOLD 2040 equsexv 2095 spimv1 2101 equsalhw 2109 aevOLD 2148 cbv3hvOLD 2161 cbv3hvOLDOLD 2162 ax6e 2238 axc15 2291 axc11nOLD 2296 axc11nOLDOLD 2297 axc11nALT 2298 ax12v2OLD 2330 sbcom2 2433 euex 2482 axext3 2592 dmi 5261 snnex 6862 1st2val 7085 2nd2val 7086 bnj1468 30170 bj-sbex 31815 bj-ssbeq 31816 bj-ssb0 31817 bj-ssb1 31822 bj-equsexval 31827 bj-ssbid2ALT 31835 bj-ax6elem2 31841 bj-eqs 31850 bj-spimtv 31905 bj-spimedv 31906 bj-spimvv 31908 bj-speiv 31911 bj-equsalv 31931 bj-dtrucor2v 31989 wl-sbcom2d 32523 wl-euequ1f 32535 axc11n-16 33241 ax12eq 33244 ax12el 33245 ax12inda 33251 ax12v2-o 33252 relexp0eq 37012 ax6e2eq 37794 relopabVD 38159 ax6e2eqVD 38165 |
Copyright terms: Public domain | W3C validator |