HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-5 958 through ax-14 968 and ax-17 969, all axioms other than ax-9 963 are believed to be theorems of free logic, although the system without ax-9 963 is probably not complete in free logic. |
| Ref | Expression |
|---|---|
| a9e |
     |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-9 963 |
. 2
 
| |
| 2 | df-ex 979 |
. 2
 
 | |
| 3 | 1, 2 | mpbir 190 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wn 2
wal 952
wceq 954
wex 978 |
| This theorem is referenced by: equvini 1166 ax11v2 1213 equid1 1267 ax11eq 1361 ax11el 1362 ax11inda 1369 a12stdy1 1370 zfext2 1459 sbcbrg 2657 axsep 2697 axsep2 2699 dtrucor2 2769 opabsb 2810 relop 3270 dmi 3321 csbima12g 3405 csbfv12g 3733 csboprg 3977 1st2val 4085 2nd2val 4086 ecelqsi 4282 axextnd 4923 csbnegg 5344 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-9 963 |
| This theorem depends on definitions: df-bi 147 df-ex 979 |