Theorem ordirr 6381

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2104   E cep 5578   Fr wfr 5627  Ord word 6362

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-eprel 5579  df-fr 5630  df-we 5632  df-ord 6366

This theorem is referenced by:  nordeq  6382  ordn2lp  6383  ordtri3or  6395  ordtri1  6396  ordtri3  6399  orddisj  6401  ordunidif  6412  ordnbtwn  6456  onirri  6476  onssneli  6479  epweon  7764  onprc  7767  nlimsucg  7833  nnlim  7871  limom  7873  soseq  8147  smo11  8366  smoord  8367  tfrlem13  8392  omopth2  8586  cofonr  8675  naddcllem  8677  limensuci  9155  infensuc  9157  ordtypelem9  9523  cantnfp1lem3  9677  cantnfp1  9678  oemapvali  9681  tskwe  9947  dif1card  10007  dju1p1e2ALT  10171  nnadju  10194  pwsdompw  10201  cflim2  10260  fin23lem24  10319  fin23lem26  10322  axdc3lem4  10450  ttukeylem7  10512  canthp1lem2  10650  inar1  10772  gruina  10815  grur1  10817  addnidpi  10898  fzennn  13937  hashp1i  14367  noseponlem  27403  noextend  27405  noextenddif  27407  noextendlt  27408  noextendgt  27409  fvnobday  27417  nosepssdm  27425  nosupbnd1lem3  27449  nosupbnd1lem5  27451  nosupbnd2lem1  27454  noinfbnd1lem3  27464  noinfbnd1lem5  27466  noinfbnd2lem1  27469  noetasuplem4  27475  noetainflem4  27479  sucneqond  36549  oaordnrex  42347  omnord1ex  42356  oenord1ex  42367  cantnfresb  42376  tfsconcatb0  42396  nlimsuc  42494