MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax1ne0 Unicode version

Theorem ax1ne0 8238
Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1ne0 8261. (Contributed by NM, 19-Mar-1996.) (New usage is discouraged.)
Assertion
Ref Expression
ax1ne0  |-  1  =/=  0

Proof of Theorem ax1ne0
StepHypRef Expression
1 1ne0sr 8174 . . . 4  |-  -.  1R  =  0R
2 1sr 8159 . . . . . 6  |-  1R  e.  R.
32elexi 2514 . . . . 5  |-  1R  e.  _V
43eqresr 8215 . . . 4  |-  ( <. 1R ,  0R >.  =  <. 0R ,  0R >.  <->  1R  =  0R )
51, 4mtbir 288 . . 3  |-  -.  <. 1R ,  0R >.  =  <. 0R ,  0R >.
6 df-1 8201 . . . 4  |-  1  =  <. 1R ,  0R >.
7 df-0 8200 . . . 4  |-  0  =  <. 0R ,  0R >.
86, 7eqeq12i 2107 . . 3  |-  ( 1  =  0  <->  <. 1R ,  0R >.  =  <. 0R ,  0R >. )
95, 8mtbir 288 . 2  |-  -.  1  =  0
10 df-ne 2214 . 2  |-  ( 1  =/=  0  <->  -.  1  =  0 )
119, 10mpbir 198 1  |-  1  =/=  0
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1525    =/= wne 2212   <.cop 3288   R.cnr 7945   0Rc0r 7946   1Rc1r 7947   0cc0 8193   1c1 8194
This theorem is referenced by:  psgnunilem4  25317
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1529  ax-11 1530  ax-13 1531  ax-14 1532  ax-17 1534  ax-12o 1568  ax-10 1582  ax-9 1588  ax-4 1595  ax-16 1781  ax-ext 2076  ax-sep 3736  ax-nul 3744  ax-pow 3780  ax-pr 3804  ax-un 4096  ax-inf2 6860
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3or 897  df-3an 898  df-tru 1259  df-ex 1451  df-sb 1742  df-eu 1964  df-mo 1965  df-clab 2082  df-cleq 2087  df-clel 2090  df-ne 2214  df-ral 2308  df-rex 2309  df-reu 2310  df-rab 2311  df-v 2507  df-sbc 2681  df-csb 2763  df-dif 2826  df-un 2828  df-in 2830  df-ss 2834  df-pss 2836  df-nul 3103  df-if 3212  df-pw 3273  df-sn 3291  df-pr 3292  df-tp 3293  df-op 3294  df-uni 3460  df-int 3494  df-iun 3537  df-br 3622  df-opab 3676  df-mpt 3677  df-tr 3709  df-eprel 3891  df-id 3895  df-po 3900  df-so 3901  df-fr 3938  df-we 3940  df-ord 3981  df-on 3982  df-lim 3983  df-suc 3984  df-om 4259  df-xp 4305  df-rel 4306  df-cnv 4307  df-co 4308  df-dm 4309  df-rn 4310  df-res 4311  df-ima 4312  df-fun 4313  df-fn 4314  df-f 4315  df-f1 4316  df-fo 4317  df-f1o 4318  df-fv 4319  df-ov 5398  df-oprab 5399  df-mpt2 5400  df-1st 5649  df-2nd 5650  df-recs 5878  df-rdg 5913  df-1o 5969  df-oadd 5973  df-omul 5974  df-er 6150  df-ec 6152  df-qs 6156  df-ni 7952  df-pli 7953  df-mi 7954  df-lti 7955  df-plpq 7988  df-mpq 7989  df-ltpq 7990  df-enq 7991  df-nq 7992  df-erq 7993  df-plq 7994  df-mq 7995  df-1nq 7996  df-rq 7997  df-ltnq 7998  df-np 8061  df-1p 8062  df-plp 8063  df-ltp 8065  df-enr 8137  df-nr 8138  df-ltr 8141  df-0r 8142  df-1r 8143  df-0 8200  df-1 8201
  Copyright terms: Public domain W3C validator