Theorem ordirr 6402

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   E cep 5583   Fr wfr 5634  Ord word 6383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-eprel 5584  df-fr 5637  df-we 5639  df-ord 6387

This theorem is referenced by:  nordeq  6403  ordn2lp  6404  ordtri3or  6416  ordtri1  6417  ordtri3  6420  orddisj  6422  ordunidif  6433  ordnbtwn  6477  onirri  6497  onssneli  6500  epweon  7795  onprc  7798  nlimsucg  7863  nnlim  7901  limom  7903  soseq  8184  smo11  8404  smoord  8405  tfrlem13  8430  omopth2  8622  cofonr  8712  naddcllem  8714  limensuci  9193  infensuc  9195  ordtypelem9  9566  cantnfp1lem3  9720  cantnfp1  9721  oemapvali  9724  tskwe  9990  dif1card  10050  dju1p1e2ALT  10215  nnadju  10238  pwsdompw  10243  cflim2  10303  fin23lem24  10362  fin23lem26  10365  axdc3lem4  10493  ttukeylem7  10555  canthp1lem2  10693  inar1  10815  gruina  10858  grur1  10860  addnidpi  10941  fzennn  14009  hashp1i  14442  noseponlem  27709  noextend  27711  noextenddif  27713  noextendlt  27714  noextendgt  27715  fvnobday  27723  nosepssdm  27731  nosupbnd1lem3  27755  nosupbnd1lem5  27757  nosupbnd2lem1  27760  noinfbnd1lem3  27770  noinfbnd1lem5  27772  noinfbnd2lem1  27775  noetasuplem4  27781  noetainflem4  27785  sucneqond  37366  oaordnrex  43308  omnord1ex  43317  oenord1ex  43328  cantnfresb  43337  tfsconcatb0  43357  nlimsuc  43454