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

Theorem ax1ne0 8106
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 8129.
Assertion
Ref Expression
ax1ne0

Proof of Theorem ax1ne0
StepHypRef Expression
1 1ne0sr 8042 . . . 4
2 1sr 8027 . . . . . 6
32elexi 2509 . . . . 5
43eqresr 8083 . . . 4
51, 4mtbir 288 . . 3
6 df-1 8069 . . . 4
7 df-0 8068 . . . 4
86, 7eqeq12i 2103 . . 3
95, 8mtbir 288 . 2
10 df-ne 2209 . 2
119, 10mpbir 198 1
Colors of variables: wff set class
Syntax hints:   wn 3   wceq 1531   wne 2207  cop 3271  cnr 7813  c0r 7814  c1r 7815  cc0 8061  c1 8062
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 1535  ax-11 1536  ax-12 1537  ax-13 1538  ax-14 1539  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-sep 3687  ax-nul 3696  ax-pow 3732  ax-pr 3756  ax-un 4049  ax-inf2 6755
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1264  df-ex 1451  df-sb 1751  df-eu 1984  df-mo 1985  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-ral 2303  df-rex 2304  df-reu 2305  df-rab 2306  df-v 2502  df-sbc 2669  df-csb 2751  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3086  df-if 3195  df-pw 3256  df-sn 3274  df-pr 3275  df-tp 3276  df-op 3277  df-uni 3435  df-int 3469  df-iun 3511  df-br 3592  df-opab 3645  df-tr 3660  df-eprel 3844  df-id 3848  df-po 3853  df-so 3854  df-fr 3891  df-we 3893  df-ord 3934  df-on 3935  df-lim 3936  df-suc 3937  df-om 4216  df-xp 4263  df-rel 4264  df-cnv 4265  df-co 4266  df-dm 4267  df-rn 4268  df-res 4269  df-ima 4270  df-fun 4271  df-fn 4272  df-f 4273  df-f1 4274  df-fo 4275  df-f1o 4276  df-fv 4277  df-ov 5298  df-oprab 5299  df-mpt 5461  df-mpt2 5462  df-1st 5613  df-2nd 5614  df-recs 5814  df-rdg 5849  df-1o 5903  df-oadd 5907  df-omul 5908  df-er 6076  df-ec 6078  df-qs 6082  df-ni 7820  df-pli 7821  df-mi 7822  df-lti 7823  df-plpq 7856  df-mpq 7857  df-ltpq 7858  df-enq 7859  df-nq 7860  df-erq 7861  df-plq 7862  df-mq 7863  df-1nq 7864  df-rq 7865  df-ltnq 7866  df-np 7929  df-1p 7930  df-plp 7931  df-ltp 7933  df-enr 8005  df-nr 8006  df-ltr 8009  df-0r 8010  df-1r 8011  df-0 8068  df-1 8069
Copyright terms: Public domain