HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem ax1ne0 8182
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 8205. (Contributed by NM, 19-Mar-1996.)
Assertion
Ref Expression
ax1ne0  |-  1  =/=  0

Proof of Theorem ax1ne0
StepHypRef Expression
1 1ne0sr 8118 . . . 4  |-  -.  1R  =  0R
2 1sr 8103 . . . . . 6  |-  1R  e.  R.
32elexi 2501 . . . . 5  |-  1R  e.  _V
43eqresr 8159 . . . 4  |-  ( <. 1R ,  0R >.  =  <. 0R ,  0R >.  <->  1R  =  0R )
51, 4mtbir 288 . . 3  |-  -.  <. 1R ,  0R >.  =  <. 0R ,  0R >.
6 df-1 8145 . . . 4  |-  1  =  <. 1R ,  0R >.
7 df-0 8144 . . . 4  |-  0  =  <. 0R ,  0R >.
86, 7eqeq12i 2095 . . 3  |-  ( 1  =  0  <->  <. 1R ,  0R >.  =  <. 0R ,  0R >. )
95, 8mtbir 288 . 2  |-  -.  1  =  0
10 df-ne 2201 . 2  |-  ( 1  =/=  0  <->  -.  1  =  0 )
119, 10mpbir 198 1  |-  1  =/=  0
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1536    =/= wne 2199   <.cop 3275   R.cnr 7889   0Rc0r 7890   1Rc1r 7891   0cc0 8137   1c1 8138
This theorem is referenced by:  psgnunilem4  23948
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-7 1453  ax-gen 1454  ax-8 1540  ax-11 1541  ax-13 1542  ax-14 1543  ax-17 1545  ax-12o 1578  ax-10 1592  ax-9 1598  ax-4 1606  ax-16 1793  ax-ext 2064  ax-sep 3715  ax-nul 3723  ax-pow 3759  ax-pr 3783  ax-un 4075  ax-inf2 6805
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 904  df-3an 905  df-tru 1268  df-ex 1456  df-sb 1754  df-eu 1976  df-mo 1977  df-clab 2070  df-cleq 2075  df-clel 2078  df-ne 2201  df-ral 2295  df-rex 2296  df-reu 2297  df-rab 2298  df-v 2494  df-sbc 2668  df-csb 2750  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3089  df-if 3199  df-pw 3260  df-sn 3278  df-pr 3279  df-tp 3280  df-op 3281  df-uni 3439  df-int 3473  df-iun 3516  df-br 3601  df-opab 3655  df-mpt 3656  df-tr 3688  df-eprel 3870  df-id 3874  df-po 3879  df-so 3880  df-fr 3917  df-we 3919  df-ord 3960  df-on 3961  df-lim 3962  df-suc 3963  df-om 4243  df-xp 4289  df-rel 4290  df-cnv 4291  df-co 4292  df-dm 4293  df-rn 4294  df-res 4295  df-ima 4296  df-fun 4297  df-fn 4298  df-f 4299  df-f1 4300  df-fo 4301  df-f1o 4302  df-fv 4303  df-ov 5357  df-oprab 5358  df-mpt2 5359  df-1st 5608  df-2nd 5609  df-recs 5835  df-rdg 5870  df-1o 5926  df-oadd 5930  df-omul 5931  df-er 6102  df-ec 6104  df-qs 6108  df-ni 7896  df-pli 7897  df-mi 7898  df-lti 7899  df-plpq 7932  df-mpq 7933  df-ltpq 7934  df-enq 7935  df-nq 7936  df-erq 7937  df-plq 7938  df-mq 7939  df-1nq 7940  df-rq 7941  df-ltnq 7942  df-np 8005  df-1p 8006  df-plp 8007  df-ltp 8009  df-enr 8081  df-nr 8082  df-ltr 8085  df-0r 8086  df-1r 8087  df-0 8144  df-1 8145
Copyright terms: Public domain