Theorem ordirr 6284

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106   E cep 5494   Fr wfr 5541  Ord word 6265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-eprel 5495  df-fr 5544  df-we 5546  df-ord 6269

This theorem is referenced by:  nordeq  6285  ordn2lp  6286  ordtri3or  6298  ordtri1  6299  ordtri3  6302  orddisj  6304  ordunidif  6314  ordnbtwn  6356  onirri  6373  onssneli  6376  epweon  7625  onprc  7628  nlimsucg  7689  nnlim  7726  limom  7728  smo11  8195  smoord  8196  tfrlem13  8221  omopth2  8415  limensuci  8940  infensuc  8942  ordtypelem9  9285  cantnfp1lem3  9438  cantnfp1  9439  oemapvali  9442  tskwe  9708  dif1card  9766  dju1p1e2ALT  9930  nnadju  9953  pwsdompw  9960  cflim2  10019  fin23lem24  10078  fin23lem26  10081  axdc3lem4  10209  ttukeylem7  10271  canthp1lem2  10409  inar1  10531  gruina  10574  grur1  10576  addnidpi  10657  fzennn  13688  hashp1i  14118  soseq  33803  naddcllem  33831  noseponlem  33867  noextend  33869  noextenddif  33871  noextendlt  33872  noextendgt  33873  fvnobday  33881  nosepssdm  33889  nosupbnd1lem3  33913  nosupbnd1lem5  33915  nosupbnd2lem1  33918  noinfbnd1lem3  33928  noinfbnd1lem5  33930  noinfbnd2lem1  33933  noetasuplem4  33939  noetainflem4  33943  sucneqond  35536  nlimsuc  41048