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 2383. When possible, use of this theorem rather than ax6e 2383 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 1972 | . 2 ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | |
2 | df-ex 1783 | . 2 ⊢ (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦) | |
3 | 1, 2 | mpbir 230 | 1 ⊢ ∃𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1537 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-6 1971 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: equs4v 2003 alequexv 2004 equsv 2006 equid 2015 ax6evr 2018 aeveq 2059 sbcom2 2161 spimedv 2190 spimfv 2232 equsalv 2259 ax6e 2383 axc15 2422 sb4b 2475 sb4bOLD 2476 dfeumo 2537 euequ 2597 dfdif3 4049 dmi 5830 1st2val 7859 2nd2val 7860 bnj1468 32826 bj-ssbeq 34834 bj-ax12 34838 bj-equsexval 34841 bj-ssbid2ALT 34844 bj-ax6elem2 34848 bj-eqs 34856 bj-equsvt 34961 bj-spimtv 34976 bj-dtrucor2v 35000 bj-sbievw1 35029 bj-sbievw 35031 wl-equsalvw 35697 wl-sbcom2d 35716 wl-euequf 35729 wl-dfclab 35747 axc11n-16 36952 ax12eq 36955 ax12el 36956 ax12inda 36962 ax12v2-o 36963 sn-el 40187 relexp0eq 41309 ax6e2eq 42177 relopabVD 42521 ax6e2eqVD 42527 dtrucor3 46144 |
Copyright terms: Public domain | W3C validator |