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

Theorem ax1ne0 7050
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 7072.
Assertion
Ref Expression
ax1ne0

Proof of Theorem ax1ne0
StepHypRef Expression
1 1ne0sr 6987 . . . 4
2 1sr 6972 . . . . . 6
32elexi 2344 . . . . 5
43eqresr 7028 . . . 4
51, 4mtbir 290 . . 3
6 df-1 7014 . . . 4
7 df-0 7013 . . . 4
86, 7eqeq12i 1942 . . 3
95, 8mtbir 290 . 2
10 df-ne 2049 . 2
119, 10mpbir 198 1
Colors of variables: wff set class
Syntax hints:   wn 3   wceq 1425   wne 2047  cop 3077  cnr 6756  c0r 6757  c1r 6758  cc0 7006  c1 7007
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-13 1433  ax-14 1434  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3795  ax-inf2 6078
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3or 913  df-3an 914  df-tru 1320  df-ex 1347  df-sb 1602  df-eu 1829  df-mo 1830  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-ral 2142  df-rex 2143  df-reu 2144  df-rab 2145  df-v 2337  df-sbc 2502  df-csb 2577  df-dif 2637  df-un 2639  df-in 2641  df-ss 2643  df-pss 2645  df-nul 2900  df-if 3005  df-pw 3063  df-sn 3080  df-pr 3081  df-tp 3082  df-op 3083  df-uni 3214  df-int 3248  df-iun 3286  df-br 3359  df-opab 3413  df-tr 3428  df-eprel 3608  df-id 3611  df-po 3616  df-so 3630  df-fr 3649  df-we 3665  df-ord 3681  df-on 3682  df-lim 3683  df-suc 3684  df-om 3958  df-xp 4005  df-rel 4006  df-cnv 4007  df-co 4008  df-dm 4009  df-rn 4010  df-res 4011  df-ima 4012  df-fun 4013  df-fn 4014  df-f 4015  df-fv 4019  df-ov 4926  df-oprab 4927  df-mpt 5063  df-mpt2 5064  df-1st 5173  df-2nd 5174  df-rdg 5363  df-1o 5400  df-oadd 5404  df-omul 5405  df-er 5537  df-ec 5539  df-qs 5543  df-ni 6763  df-pli 6764  df-mi 6765  df-lti 6766  df-plpq 6799  df-mpq 6800  df-ltpq 6801  df-enq 6802  df-nq 6803  df-erq 6804  df-plq 6805  df-mq 6806  df-1nq 6807  df-rq 6808  df-ltnq 6809  df-np 6873  df-1p 6874  df-plp 6875  df-ltp 6877  df-enr 6949  df-nr 6950  df-ltr 6953  df-0r 6954  df-1r 6955  df-0 7013  df-1 7014
Copyright terms: Public domain