Theorem ordirr 6329

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   E cep 5522   Fr wfr 5573  Ord word 6310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-eprel 5523  df-fr 5576  df-we 5578  df-ord 6314

This theorem is referenced by:  nordeq  6330  ordn2lp  6331  ordtri3or  6343  ordtri1  6344  ordtri3  6347  orddisj  6349  ordunidif  6361  ordnbtwn  6406  onirri  6425  onssneli  6428  epweon  7715  onprc  7718  nlimsucg  7782  nnlim  7820  limom  7822  soseq  8099  smo11  8294  smoord  8295  tfrlem13  8319  omopth2  8509  cofonr  8599  naddcllem  8601  limensuci  9077  infensuc  9079  ordtypelem9  9437  cantnfp1lem3  9595  cantnfp1  9596  oemapvali  9599  tskwe  9865  dif1card  9923  dju1p1e2ALT  10088  nnadju  10111  pwsdompw  10116  cflim2  10176  fin23lem24  10235  fin23lem26  10238  axdc3lem4  10366  ttukeylem7  10428  canthp1lem2  10566  inar1  10688  gruina  10731  grur1  10733  addnidpi  10814  fzennn  13893  hashp1i  14328  noseponlem  27592  noextend  27594  noextenddif  27596  noextendlt  27597  noextendgt  27598  fvnobday  27606  nosepssdm  27614  nosupbnd1lem3  27638  nosupbnd1lem5  27640  nosupbnd2lem1  27643  noinfbnd1lem3  27653  noinfbnd1lem5  27655  noinfbnd2lem1  27658  noetasuplem4  27664  noetainflem4  27668  sucneqond  37341  oaordnrex  43271  omnord1ex  43280  oenord1ex  43291  cantnfresb  43300  tfsconcatb0  43320  nlimsuc  43417