Theorem 0elon 5778

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

Assertion

Ref	Expression
0elon	⊢ ∅ ∈ On

Proof of Theorem 0elon

Step	Hyp	Ref	Expression
1		ord0 5777	. 2 ⊢ Ord ∅
2		0ex 4790	. . 3 ⊢ ∅ ∈ V
3	2	elon 5732	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 221	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 1990  ∅c0 3915  Ord word 5722  Oncon0 5723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916  df-pw 4160  df-uni 4437  df-tr 4753  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-ord 5726  df-on 5727

This theorem is referenced by:  inton  5782  onn0  5789  on0eqel  5845  orduninsuc  7043  onzsl  7046  smofvon2  7453  tfrlem16  7489  1on  7567  ordgt0ge1  7577  oa0  7596  om0  7597  oe0m  7598  oe0m0  7600  oe0  7602  oesuclem  7605  omcl  7616  oecl  7617  oa0r  7618  om0r  7619  oaord1  7631  oaword1  7632  oaword2  7633  oawordeu  7635  oa00  7639  odi  7659  oeoa  7677  oeoe  7679  nna0r  7689  nnm0r  7690  card2on  8459  card2inf  8460  harcl  8466  cantnfvalf  8562  rankon  8658  cardon  8770  card0  8784  alephon  8892  alephgeom  8905  alephfplem1  8927  cdafi  9012  ttukeylem4  9334  ttukeylem7  9337  cfpwsdom  9406  inar1  9597  rankcf  9599  gruina  9640  bnj168  30798  rdgprc0  31699  sltval2  31809  sltsolem1  31826  nosepnelem  31830  nodense  31842  nolt02o  31845  bdayelon  31892  rankeq1o  32278  0hf  32284  onsucconn  32437  onsucsuccmp  32443  finxp1o  33229  finxpreclem4  33231  harn0  37672