![]() |
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 2286. When possible, use of this theorem rather than ax6e 2286 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 1946 | . 2 ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | |
2 | df-ex 1745 | . 2 ⊢ (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦) | |
3 | 1, 2 | mpbir 221 | 1 ⊢ ∃𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1521 ∃wex 1744 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-6 1945 |
This theorem depends on definitions: df-bi 197 df-ex 1745 |
This theorem is referenced by: exiftru 1948 spimeh 1971 equs4v 1976 equsalvw 1977 equsexvw 1978 equid 1985 ax6evr 1988 equvinv 2003 aeveq 2024 19.8a 2090 equsalv 2146 equsexv 2147 spimv1 2153 equsalhw 2161 ax6e 2286 axc15 2339 axc11nOLD 2343 sbcom2 2473 euex 2522 axext3 2633 dmi 5372 snnexOLD 7009 1st2val 7238 2nd2val 7239 bnj1468 31042 bj-sbex 32751 bj-ssbeq 32752 bj-ssb0 32753 bj-ssb1 32758 bj-equsexval 32763 bj-ssbid2ALT 32771 bj-ax6elem2 32777 bj-alequexv 32780 bj-eqs 32788 bj-spimtv 32843 bj-spimedv 32844 bj-spimvv 32846 bj-speiv 32849 bj-dtrucor2v 32926 bj-cleljustab 32972 wl-sbcom2d 33474 wl-euequ1f 33486 axc11n-16 34542 ax12eq 34545 ax12el 34546 ax12inda 34552 ax12v2-o 34553 relexp0eq 38310 ax6e2eq 39090 relopabVD 39451 ax6e2eqVD 39457 |
Copyright terms: Public domain | W3C validator |