Theorem ordirr 6331

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113   E cep 5520   Fr wfr 5571  Ord word 6312

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 2115  ax-9 2123  ax-ext 2705  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 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-eprel 5521  df-fr 5574  df-we 5576  df-ord 6316

This theorem is referenced by:  nordeq  6332  ordn2lp  6333  ordtri3or  6345  ordtri1  6346  ordtri3  6349  orddisj  6351  ordunidif  6363  ordnbtwn  6408  onirri  6427  onssneli  6430  epweon  7716  onprc  7719  nlimsucg  7780  nnlim  7818  limom  7820  soseq  8097  smo11  8292  smoord  8293  tfrlem13  8317  omopth2  8507  cofonr  8597  naddcllem  8599  limensuci  9075  infensuc  9077  ordtypelem9  9421  cantnfp1lem3  9579  cantnfp1  9580  oemapvali  9583  tskwe  9852  dif1card  9910  dju1p1e2ALT  10075  nnadju  10098  pwsdompw  10103  cflim2  10163  fin23lem24  10222  fin23lem26  10225  axdc3lem4  10353  ttukeylem7  10415  canthp1lem2  10553  inar1  10675  gruina  10718  grur1  10720  addnidpi  10801  fzennn  13879  hashp1i  14314  noseponlem  27606  noextend  27608  noextenddif  27610  noextendlt  27611  noextendgt  27612  fvnobday  27620  nosepssdm  27628  nosupbnd1lem3  27652  nosupbnd1lem5  27654  nosupbnd2lem1  27657  noinfbnd1lem3  27667  noinfbnd1lem5  27669  noinfbnd2lem1  27672  noetasuplem4  27678  noetainflem4  27682  sucneqond  37432  oaordnrex  43415  omnord1ex  43424  oenord1ex  43435  cantnfresb  43444  tfsconcatb0  43464  nlimsuc  43561