![]() |
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 2391. When possible, use of this theorem rather than ax6e 2391 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 1968 | . 2 ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | |
2 | df-ex 1778 | . 2 ⊢ (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦) | |
3 | 1, 2 | mpbir 231 | 1 ⊢ ∃𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1535 ∃wex 1777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-6 1967 |
This theorem depends on definitions: df-bi 207 df-ex 1778 |
This theorem is referenced by: equs4v 1999 alequexv 2000 equsv 2002 equid 2011 ax6evr 2014 aeveq 2056 sbcom2 2174 spimedv 2198 spimfv 2240 equsalv 2268 ax6e 2391 axc15 2430 sb4b 2483 dfeumo 2540 euequ 2600 dfdif3OLD 4141 exel 5453 dmi 5946 1st2val 8060 2nd2val 8061 bnj1468 34824 in-ax8 36192 ss-ax8 36193 bj-ssbeq 36621 bj-ax12 36625 bj-equsexval 36628 bj-ssbid2ALT 36631 bj-ax6elem2 36635 bj-eqs 36643 bj-equsvt 36747 bj-spimtv 36762 bj-dtrucor2v 36785 bj-sbievw1 36813 bj-sbievw 36815 wl-equsalvw 37494 wl-equsaldv 37496 wl-sbcom2d 37517 wl-euequf 37530 wl-dfclab 37552 axc11n-16 38896 ax12eq 38899 ax12el 38900 ax12inda 38906 ax12v2-o 38907 sn-exelALT 42213 relexp0eq 43665 ax6e2eq 44530 relopabVD 44874 ax6e2eqVD 44880 dtrucor3 48534 |
Copyright terms: Public domain | W3C validator |