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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111   E cep 5515   Fr wfr 5566  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 5234  ax-nul 5244  ax-pr 5370

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 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-eprel 5516  df-fr 5569  df-we 5571  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  27604  noextend  27606  noextenddif  27608  noextendlt  27609  noextendgt  27610  fvnobday  27618  nosepssdm  27626  nosupbnd1lem3  27650  nosupbnd1lem5  27652  nosupbnd2lem1  27655  noinfbnd1lem3  27665  noinfbnd1lem5  27667  noinfbnd2lem1  27670  noetasuplem4  27676  noetainflem4  27680  sucneqond  37405  oaordnrex  43334  omnord1ex  43343  oenord1ex  43354  cantnfresb  43363  tfsconcatb0  43383  nlimsuc  43480