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

Theorem ax1ne0 7256
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 7278.
Assertion
Ref Expression
ax1ne0

Proof of Theorem ax1ne0
StepHypRef Expression
1 1ne0sr 7193 . . . 4
2 1sr 7178 . . . . . 6
32elexi 2335 . . . . 5
43eqresr 7234 . . . 4
51, 4mtbir 288 . . 3
6 df-1 7220 . . . 4
7 df-0 7219 . . . 4
86, 7eqeq12i 1931 . . 3
95, 8mtbir 288 . 2
10 df-ne 2037 . 2
119, 10mpbir 198 1
Colors of variables: wff set class
Syntax hints:   wn 3   wceq 1414   wne 2035  cop 3086  cnr 6962  c0r 6963  c1r 6964  cc0 7212  c1 7213
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-13 1422  ax-14 1423  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-rep 3469  ax-sep 3479  ax-nul 3488  ax-pow 3524  ax-pr 3548  ax-un 3823  ax-inf2 6256
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1309  df-ex 1336  df-sb 1591  df-eu 1818  df-mo 1819  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-ral 2131  df-rex 2132  df-reu 2133  df-rab 2134  df-v 2328  df-sbc 2495  df-csb 2577  df-dif 2639  df-un 2641  df-in 2643  df-ss 2647  df-pss 2649  df-nul 2905  df-if 3012  df-pw 3072  df-sn 3089  df-pr 3090  df-tp 3091  df-op 3092  df-uni 3234  df-int 3268  df-iun 3307  df-br 3384  df-opab 3438  df-tr 3453  df-eprel 3634  df-id 3637  df-po 3642  df-so 3656  df-fr 3676  df-we 3692  df-ord 3708  df-on 3709  df-lim 3710  df-suc 3711  df-om 3988  df-xp 4035  df-rel 4036  df-cnv 4037  df-co 4038  df-dm 4039  df-rn 4040  df-res 4041  df-ima 4042  df-fun 4043  df-fn 4044  df-f 4045  df-fv 4049  df-ov 5004  df-oprab 5005  df-mpt 5165  df-mpt2 5166  df-1st 5296  df-2nd 5297  df-rdg 5498  df-1o 5535  df-oadd 5539  df-omul 5540  df-er 5673  df-ec 5675  df-qs 5679  df-ni 6969  df-pli 6970  df-mi 6971  df-lti 6972  df-plpq 7005  df-mpq 7006  df-ltpq 7007  df-enq 7008  df-nq 7009  df-erq 7010  df-plq 7011  df-mq 7012  df-1nq 7013  df-rq 7014  df-ltnq 7015  df-np 7079  df-1p 7080  df-plp 7081  df-ltp 7083  df-enr 7155  df-nr 7156  df-ltr 7159  df-0r 7160  df-1r 7161  df-0 7219  df-1 7220
Copyright terms: Public domain