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

Theorem ax1ne0 7004
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 7026.
Assertion
Ref Expression
ax1ne0 |- 1 =/= 0

Proof of Theorem ax1ne0
StepHypRef Expression
1 1ne0sr 6941 . . . 4 |- -. 1R = 0R
2 1sr 6926 . . . . . 6 |- 1R e. R.
32elexi 2374 . . . . 5 |- 1R e. _V
43eqresr 6982 . . . 4 |- (<.1R, 0R>. = <.0R, 0R>. <-> 1R = 0R)
51, 4mtbir 312 . . 3 |- -. <.1R, 0R>. = <.0R, 0R>.
6 df-1 6968 . . . 4 |- 1 = <.1R, 0R>.
7 df-0 6967 . . . 4 |- 0 = <.0R, 0R>.
86, 7eqeq12i 1973 . . 3 |- (1 = 0 <-> <.1R, 0R>. = <.0R, 0R>.)
95, 8mtbir 312 . 2 |- -. 1 = 0
10 df-ne 2080 . 2 |- (1 =/= 0 <-> -. 1 = 0)
119, 10mpbir 218 1 |- 1 =/= 0
Colors of variables: wff set class
Syntax hints:  -. wn 3   = wceq 1457   =/= wne 2078  <.cop 3097  R.cnr 6710  0Rc0r 6711  1Rc1r 6712  0cc0 6960  1c1 6961
This theorem is referenced by:  axlowdimlem13 14454  axlowdimlem14 14455  axlowdim1 14459
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-13 1465  ax-14 1466  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1671  ax-ext 1942  ax-rep 3462  ax-sep 3472  ax-nul 3481  ax-pow 3517  ax-pr 3541  ax-un 3811  ax-inf2 6033
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3or 947  df-3an 948  df-tru 1354  df-ex 1381  df-sb 1633  df-eu 1860  df-mo 1861  df-clab 1948  df-cleq 1953  df-clel 1956  df-ne 2080  df-ral 2173  df-rex 2174  df-reu 2175  df-rab 2176  df-v 2367  df-sbc 2532  df-csb 2606  df-dif 2665  df-un 2667  df-in 2669  df-ss 2671  df-pss 2673  df-nul 2927  df-if 3028  df-pw 3084  df-sn 3099  df-pr 3100  df-tp 3102  df-op 3103  df-uni 3232  df-int 3266  df-iun 3304  df-br 3377  df-opab 3431  df-tr 3446  df-eprel 3624  df-id 3627  df-po 3632  df-so 3646  df-fr 3665  df-we 3681  df-ord 3697  df-on 3698  df-lim 3699  df-suc 3700  df-om 3967  df-xp 4014  df-rel 4015  df-cnv 4016  df-co 4017  df-dm 4018  df-rn 4019  df-res 4020  df-ima 4021  df-fun 4022  df-fn 4023  df-f 4024  df-fv 4028  df-ov 4926  df-oprab 4927  df-mpt 5061  df-mpt2 5062  df-1st 5130  df-2nd 5131  df-rdg 5320  df-1o 5357  df-oadd 5361  df-omul 5362  df-er 5494  df-ec 5496  df-qs 5500  df-ni 6717  df-pli 6718  df-mi 6719  df-lti 6720  df-plpq 6753  df-mpq 6754  df-ltpq 6755  df-enq 6756  df-nq 6757  df-erq 6758  df-plq 6759  df-mq 6760  df-1nq 6761  df-rq 6762  df-ltnq 6763  df-np 6827  df-1p 6828  df-plp 6829  df-ltp 6831  df-enr 6903  df-nr 6904  df-ltr 6907  df-0r 6908  df-1r 6909  df-0 6967  df-1 6968
Copyright terms: Public domain