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

Theorem ax1ne0 7151
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 7173.
Assertion
Ref Expression
ax1ne0

Proof of Theorem ax1ne0
StepHypRef Expression
1 1ne0sr 7088 . . . 4
2 1sr 7073 . . . . . 6
32elexi 2331 . . . . 5
43eqresr 7129 . . . 4
51, 4mtbir 287 . . 3
6 df-1 7115 . . . 4
7 df-0 7114 . . . 4
86, 7eqeq12i 1930 . . 3
95, 8mtbir 287 . 2
10 df-ne 2036 . 2
119, 10mpbir 197 1
Colors of variables: wff set class
Syntax hints:   wn 3   wceq 1413   wne 2034  cop 3076  cnr 6857  c0r 6858  c1r 6859  cc0 7107  c1 7108
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-13 1421  ax-14 1422  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3797  ax-inf2 6154
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3or 899  df-3an 900  df-tru 1308  df-ex 1335  df-sb 1590  df-eu 1817  df-mo 1818  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-ral 2129  df-rex 2130  df-reu 2131  df-rab 2132  df-v 2324  df-sbc 2491  df-csb 2573  df-dif 2635  df-un 2637  df-in 2639  df-ss 2641  df-pss 2643  df-nul 2899  df-if 3004  df-pw 3062  df-sn 3079  df-pr 3080  df-tp 3081  df-op 3082  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 3650  df-we 3666  df-ord 3682  df-on 3683  df-lim 3684  df-suc 3685  df-om 3962  df-xp 4009  df-rel 4010  df-cnv 4011  df-co 4012  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fun 4017  df-fn 4018  df-f 4019  df-fv 4023  df-ov 4946  df-oprab 4947  df-mpt 5106  df-mpt2 5107  df-1st 5231  df-2nd 5232  df-rdg 5424  df-1o 5461  df-oadd 5465  df-omul 5466  df-er 5598  df-ec 5600  df-qs 5604  df-ni 6864  df-pli 6865  df-mi 6866  df-lti 6867  df-plpq 6900  df-mpq 6901  df-ltpq 6902  df-enq 6903  df-nq 6904  df-erq 6905  df-plq 6906  df-mq 6907  df-1nq 6908  df-rq 6909  df-ltnq 6910  df-np 6974  df-1p 6975  df-plp 6976  df-ltp 6978  df-enr 7050  df-nr 7051  df-ltr 7054  df-0r 7055  df-1r 7056  df-0 7114  df-1 7115
Copyright terms: Public domain