Theorem 0elon 6449

Description: The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 17-Sep-1993.)

Assertion

Ref	Expression
0elon	⊢ ∅ ∈ On

Proof of Theorem 0elon

Step	Hyp	Ref	Expression
1		ord0 6448	. 2 ⊢ Ord ∅
2		0ex 5325	. . 3 ⊢ ∅ ∈ V
3	2	elon 6404	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 231	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2108  ∅c0 4352  Ord word 6394  Oncon0 6395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-tr 5284  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399

This theorem is referenced by:  inton  6453  onn0  6460  on0eqel  6519  orduninsuc  7880  onzsl  7883  peano1  7927  smofvon2  8412  tfrlem16  8449  rdg0n  8490  1on  8534  1onOLD  8535  ordgt0ge1  8549  oa0  8572  om0  8573  oe0m  8574  oe0m0  8576  oe0  8578  oesuclem  8581  omcl  8592  oecl  8593  oa0r  8594  om0r  8595  oaord1  8607  oaword1  8608  oaword2  8609  oawordeu  8611  oa00  8615  odi  8635  oeoa  8653  oeoe  8655  nna0r  8665  nnm0r  8666  naddrid  8739  naddlid  8740  naddword1  8747  card2on  9623  card2inf  9624  harcl  9628  cantnfvalf  9734  rankon  9864  cardon  10013  card0  10027  alephon  10138  alephgeom  10151  alephfplem1  10173  djufi  10256  ttukeylem4  10581  ttukeylem7  10584  cfpwsdom  10653  inar1  10844  rankcf  10846  gruina  10887  sltval2  27719  sltsolem1  27738  nosepnelem  27742  nodense  27755  nolt02o  27758  bdayelon  27839  cuteq1  27896  old0  27916  made0  27930  old1  27932  mulsproplem2  28161  mulsproplem3  28162  mulsproplem4  28163  mulsproplem5  28164  mulsproplem6  28165  mulsproplem7  28166  mulsproplem8  28167  mulsproplem12  28171  mulsproplem13  28172  mulsproplem14  28173  precsexlem1  28249  precsexlem2  28250  bnj168  34706  rdgprc0  35757  rankeq1o  36135  0hf  36141  onsucconn  36404  onsucsuccmp  36410  finxp1o  37358  finxpreclem4  37360  harn0  43059  onexoegt  43205  ordeldif1o  43222  oe0suclim  43239  oaordnr  43258  nnoeomeqom  43274  oenass  43281  omabs2  43294  omcl3g  43296  naddcnff  43324  nadd2rabex  43348  safesnsupfiss  43377  safesnsupfidom1o  43379  safesnsupfilb  43380  0no  43397  nlim1NEW  43404  aleph1min  43519