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 2113   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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  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  7720  onprc  7723  nlimsucg  7784  nnlim  7822  limom  7824  soseq  8101  smo11  8296  smoord  8297  tfrlem13  8321  omopth2  8511  cofonr  8602  naddcllem  8604  limensuci  9081  infensuc  9083  ordtypelem9  9431  cantnfp1lem3  9589  cantnfp1  9590  oemapvali  9593  tskwe  9862  dif1card  9920  dju1p1e2ALT  10085  nnadju  10108  pwsdompw  10113  cflim2  10173  fin23lem24  10232  fin23lem26  10235  axdc3lem4  10363  ttukeylem7  10425  canthp1lem2  10564  inar1  10686  gruina  10729  grur1  10731  addnidpi  10812  fzennn  13891  hashp1i  14326  noseponlem  27632  noextend  27634  noextenddif  27636  noextendlt  27637  noextendgt  27638  fvnobday  27646  nosepssdm  27654  nosupbnd1lem3  27678  nosupbnd1lem5  27680  nosupbnd2lem1  27683  noinfbnd1lem3  27693  noinfbnd1lem5  27695  noinfbnd2lem1  27698  noetasuplem4  27704  noetainflem4  27708  sucneqond  37570  oaordnrex  43537  omnord1ex  43546  oenord1ex  43557  cantnfresb  43566  tfsconcatb0  43586  nlimsuc  43682