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 2394. When possible, use of this theorem rather than ax6e 2394 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 1962 | . 2 ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | |
2 | df-ex 1772 | . 2 ⊢ (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦) | |
3 | 1, 2 | mpbir 232 | 1 ⊢ ∃𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1526 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-6 1961 |
This theorem depends on definitions: df-bi 208 df-ex 1772 |
This theorem is referenced by: spimehOLD 1966 exgenOLD 1970 equs4v 1997 alequexv 1998 equsv 2000 equsexvwOLD 2003 equid 2010 ax6evr 2013 aeveq 2052 spsbeOLD 2080 sbcom2 2158 spimedv 2188 spimfv 2232 equsalv 2259 equsexv 2260 ax6e 2394 axc15 2438 axc15OLD 2439 sb4b 2495 sb4bOLD 2496 equsb1vOLDOLD 2513 sbtvOLD 2515 dfeumo 2615 euequ 2679 dfdif3 4090 dmi 5785 1st2val 7708 2nd2val 7709 bnj1468 32018 bj-ssbeq 33884 bj-ax12 33888 bj-equsexval 33891 bj-ssbid2ALT 33894 bj-ax6elem2 33898 bj-eqs 33906 bj-spimtv 34014 bj-dtrucor2v 34038 bj-sbievw1 34067 bj-sbievw 34069 wl-equsalvw 34660 wl-sbcom2d 34679 wl-euequf 34692 wl-dfclab 34710 axc11n-16 35956 ax12eq 35959 ax12el 35960 ax12inda 35966 ax12v2-o 35967 sn-el 38990 relexp0eq 39926 ax6e2eq 40771 relopabVD 41115 ax6e2eqVD 41121 |
Copyright terms: Public domain | W3C validator |