Theorem ordirr 4578

Description: Epsilon irreflexivity of ordinals: no ordinal class is a member of itself. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. The present proof requires ax-setind 4573. If in the definition of ordinals df-iord 4401, we also required that membership be well-founded on any ordinal (see df-frind 4367), then we could prove ordirr 4578 without ax-setind 4573. (Contributed by NM, 2-Jan-1994.)

Assertion

Ref	Expression
ordirr	|- ( Ord A -> -. A e. A )

Proof of Theorem ordirr

Step	Hyp	Ref	Expression
1		elirr 4577	. 2 |- -. A e. A
2	1	a1i 9	1 |- ( Ord A -> -. A e. A )

Syntax hints:   -. wn 3   -> wi 4   e. wcel 2167   Ord word 4397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-setind 4573

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-ral 2480  df-v 2765  df-dif 3159  df-sn 3628

This theorem is referenced by:  onirri  4579  nordeq  4580  ordn2lp  4581  orddisj  4582  onprc  4588  nlimsucg  4602  tfr1onlemsucfn  6398  tfr1onlemsucaccv  6399  tfrcllemsucfn  6411  tfrcllemsucaccv  6412  nntr2  6561  unsnfi  6980  nnnninfeq  7194  nninfisol  7199  addnidpig  7403  frecfzennn  10518  hashinfom  10870  hashennn  10872  hashp1i  10902  ennnfonelemg  12620  ctinfom  12645