Theorem ordirr 6413

Description: No ordinal class is a member of itself. In other words, the membership relation is irreflexive on ordinal classes. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. Theorem 1.9(i) of [Schloeder] p. 1. We prove this without invoking the Axiom of Regularity. (Contributed by NM, 2-Jan-1994.)

Assertion

Ref	Expression
ordirr	⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)

Proof of Theorem ordirr

Step	Hyp	Ref	Expression
1		ordfr 6410	. 2 ⊢ (Ord 𝐴 → E Fr 𝐴)
2		efrirr 5680	. 2 ⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴)
3	1, 2	syl 17	1 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   E cep 5598   Fr wfr 5649  Ord word 6394

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-sep 5317  ax-nul 5324  ax-pr 5447

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-br 5167  df-opab 5229  df-eprel 5599  df-fr 5652  df-we 5654  df-ord 6398

This theorem is referenced by:  nordeq  6414  ordn2lp  6415  ordtri3or  6427  ordtri1  6428  ordtri3  6431  orddisj  6433  ordunidif  6444  ordnbtwn  6488  onirri  6508  onssneli  6511  epweon  7810  onprc  7813  nlimsucg  7879  nnlim  7917  limom  7919  soseq  8200  smo11  8420  smoord  8421  tfrlem13  8446  omopth2  8640  cofonr  8730  naddcllem  8732  limensuci  9219  infensuc  9221  ordtypelem9  9595  cantnfp1lem3  9749  cantnfp1  9750  oemapvali  9753  tskwe  10019  dif1card  10079  dju1p1e2ALT  10244  nnadju  10267  pwsdompw  10272  cflim2  10332  fin23lem24  10391  fin23lem26  10394  axdc3lem4  10522  ttukeylem7  10584  canthp1lem2  10722  inar1  10844  gruina  10887  grur1  10889  addnidpi  10970  fzennn  14019  hashp1i  14452  noseponlem  27727  noextend  27729  noextenddif  27731  noextendlt  27732  noextendgt  27733  fvnobday  27741  nosepssdm  27749  nosupbnd1lem3  27773  nosupbnd1lem5  27775  nosupbnd2lem1  27778  noinfbnd1lem3  27788  noinfbnd1lem5  27790  noinfbnd2lem1  27793  noetasuplem4  27799  noetainflem4  27803  sucneqond  37331  oaordnrex  43257  omnord1ex  43266  oenord1ex  43277  cantnfresb  43286  tfsconcatb0  43306  nlimsuc  43403