Theorem 1n0 6528

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 6525	. 2 ⊢ 1o = {∅}
2		0ex 4176	. . 3 ⊢ ∅ ∈ V
3	2	snnz 3754	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 2400	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2377  ∅c0 3462  {csn 3635  1_oc1o 6505

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 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-nul 4175

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-v 2775  df-dif 3170  df-un 3172  df-nul 3463  df-sn 3641  df-suc 4423  df-1o 6512

This theorem is referenced by:  xp01disj  6529  xp01disjl  6530  rex2dom  6921  djulclb  7169  djuinr  7177  eldju2ndl  7186  djune  7192  updjudhf  7193  updjudhcoinrg  7195  nninfisollemne  7245  nninfisol  7247  exmidomni  7256  fodjum  7260  fodju0  7261  ismkvnex  7269  mkvprop  7272  omniwomnimkv  7281  nninfwlporlemd  7286  nninfwlpoimlemginf  7290  2oneel  7381  1pi  7441  nninfinf  10601  unct  12863  fnpr2o  13221  fnpr2ob  13222  fvpr0o  13223  fvpr1o  13224  fvprif  13225  xpsfrnel  13226  bj-charfunbi  15861  2omap  16047  pwle2  16050  subctctexmid  16052  pw1nct  16055  peano3nninf  16059  nninfalllem1  16060  nninfall  16061  nninfsellemeq  16066  nninfsellemqall  16067  nninffeq  16072