Theorem 1n0 6599

Description: Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.)

Assertion

Ref	Expression
1n0	|- 1o =/= (/)

Proof of Theorem 1n0

Step	Hyp	Ref	Expression
1		df1o2 6595	. 2 |- 1o = { (/) }
2		0ex 4216	. . 3 |- (/) e. _V
3	2	snnz 3791	. 2 |- { (/) } =/= (/)
4	1, 3	eqnetri 2425	1 |- 1o =/= (/)

Syntax hints:   =/= wne 2402   (/)c0 3494   {csn 3669   1oc1o 6574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-nul 4215

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-v 2804  df-dif 3202  df-un 3204  df-nul 3495  df-sn 3675  df-suc 4468  df-1o 6581

This theorem is referenced by:  xp01disj  6600  xp01disjl  6601  rex2dom  6995  djulclb  7253  djuinr  7261  eldju2ndl  7270  djune  7276  updjudhf  7277  updjudhcoinrg  7279  nninfisollemne  7329  nninfisol  7331  exmidomni  7340  fodjum  7344  fodju0  7345  ismkvnex  7353  mkvprop  7356  omniwomnimkv  7365  nninfwlporlemd  7370  nninfwlpoimlemginf  7374  pr2cv1  7399  2oneel  7474  1pi  7534  nninfinf  10704  unct  13062  fnpr2o  13421  fnpr2ob  13422  fvpr0o  13423  fvpr1o  13424  fvprif  13425  xpsfrnel  13426  bj-charfunbi  16406  3dom  16587  2omap  16594  pwle2  16599  subctctexmid  16601  pw1nct  16604  peano3nninf  16609  nninfalllem1  16610  nninfall  16611  nninfsellemeq  16616  nninfsellemqall  16617  nninffeq  16622