Theorem ordirr 6324

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 6321	. 2 ⊢ (Ord 𝐴 → E Fr 𝐴)
2		efrirr 5594	. 2 ⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴)
3	1, 2	syl 17	1 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111   E cep 5513   Fr wfr 5564  Ord word 6305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-eprel 5514  df-fr 5567  df-we 5569  df-ord 6309

This theorem is referenced by:  nordeq  6325  ordn2lp  6326  ordtri3or  6338  ordtri1  6339  ordtri3  6342  orddisj  6344  ordunidif  6356  ordnbtwn  6401  onirri  6420  onssneli  6423  epweon  7708  onprc  7711  nlimsucg  7772  nnlim  7810  limom  7812  soseq  8089  smo11  8284  smoord  8285  tfrlem13  8309  omopth2  8499  cofonr  8589  naddcllem  8591  limensuci  9066  infensuc  9068  ordtypelem9  9412  cantnfp1lem3  9570  cantnfp1  9571  oemapvali  9574  tskwe  9843  dif1card  9901  dju1p1e2ALT  10066  nnadju  10089  pwsdompw  10094  cflim2  10154  fin23lem24  10213  fin23lem26  10216  axdc3lem4  10344  ttukeylem7  10406  canthp1lem2  10544  inar1  10666  gruina  10709  grur1  10711  addnidpi  10792  fzennn  13875  hashp1i  14310  noseponlem  27603  noextend  27605  noextenddif  27607  noextendlt  27608  noextendgt  27609  fvnobday  27617  nosepssdm  27625  nosupbnd1lem3  27649  nosupbnd1lem5  27651  nosupbnd2lem1  27654  noinfbnd1lem3  27664  noinfbnd1lem5  27666  noinfbnd2lem1  27669  noetasuplem4  27675  noetainflem4  27679  sucneqond  37409  oaordnrex  43398  omnord1ex  43407  oenord1ex  43418  cantnfresb  43427  tfsconcatb0  43447  nlimsuc  43544