Theorem ordirr 6335

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   E cep 5523   Fr wfr 5574  Ord word 6316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-eprel 5524  df-fr 5577  df-we 5579  df-ord 6320

This theorem is referenced by:  nordeq  6336  ordn2lp  6337  ordtri3or  6349  ordtri1  6350  ordtri3  6353  orddisj  6355  ordunidif  6367  ordnbtwn  6412  onirri  6431  onssneli  6434  epweon  7722  onprc  7725  nlimsucg  7786  nnlim  7824  limom  7826  soseq  8102  smo11  8297  smoord  8298  tfrlem13  8322  omopth2  8512  cofonr  8603  naddcllem  8605  limensuci  9084  infensuc  9086  ordtypelem9  9434  cantnfp1lem3  9592  cantnfp1  9593  oemapvali  9596  tskwe  9865  dif1card  9923  dju1p1e2ALT  10088  nnadju  10111  pwsdompw  10116  cflim2  10176  fin23lem24  10235  fin23lem26  10238  axdc3lem4  10366  ttukeylem7  10428  canthp1lem2  10567  inar1  10689  gruina  10732  grur1  10734  addnidpi  10815  fzennn  13921  hashp1i  14356  noseponlem  27642  noextend  27644  noextenddif  27646  noextendlt  27647  noextendgt  27648  fvnobday  27656  nosepssdm  27664  nosupbnd1lem3  27688  nosupbnd1lem5  27690  nosupbnd2lem1  27693  noinfbnd1lem3  27703  noinfbnd1lem5  27705  noinfbnd2lem1  27708  noetasuplem4  27714  noetainflem4  27718  sucneqond  37695  oaordnrex  43741  omnord1ex  43750  oenord1ex  43761  cantnfresb  43770  tfsconcatb0  43790  nlimsuc  43886