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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2119   E cep 5524   Fr wfr 5575  Ord word 6316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-eprel 5525  df-fr 5578  df-we 5580  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  7725  onprc  7728  nlimsucg  7789  nnlim  7827  limom  7829  soseq  8106  smo11  8301  smoord  8302  tfrlem13  8326  omopth2  8516  cofonr  8607  naddcllem  8609  limensuci  9088  infensuc  9090  ordtypelem9  9438  cantnfp1lem3  9599  cantnfp1  9600  oemapvali  9603  tskwe  9872  dif1card  9930  dju1p1e2ALT  10095  nnadju  10118  pwsdompw  10123  cflim2  10183  fin23lem24  10242  fin23lem26  10245  axdc3lem4  10373  ttukeylem7  10435  canthp1lem2  10574  inar1  10696  gruina  10739  grur1  10741  addnidpi  10822  fzennn  13928  hashp1i  14363  noseponlem  27653  noextend  27655  noextenddif  27657  noextendlt  27658  noextendgt  27659  fvnobday  27667  nosepssdm  27675  nosupbnd1lem3  27699  nosupbnd1lem5  27701  nosupbnd2lem1  27704  noinfbnd1lem3  27714  noinfbnd1lem5  27716  noinfbnd2lem1  27719  noetasuplem4  27725  noetainflem4  27729  bj-iomnnom  37626  sucneqond  37734  oaordnrex  43747  omnord1ex  43756  oenord1ex  43767  cantnfresb  43776  omabs2  43784  tfsconcatb0  43796  nlimsuc  43892