Theorem ordirr 4579

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 4574. If in the definition of ordinals df-iord 4402, we also required that membership be well-founded on any ordinal (see df-frind 4368), then we could prove ordirr 4579 without ax-setind 4574. (Contributed by NM, 2-Jan-1994.)

Assertion

Ref	Expression
ordirr	⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)

Proof of Theorem ordirr

Step	Hyp	Ref	Expression
1		elirr 4578	. 2 ⊢ ¬ 𝐴 ∈ 𝐴
2	1	a1i 9	1 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2167  Ord word 4398

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 4574

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 3629

This theorem is referenced by:  onirri  4580  nordeq  4581  ordn2lp  4582  orddisj  4583  onprc  4589  nlimsucg  4603  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  nntr2  6570  unsnfi  6989  nnnninfeq  7203  nninfisol  7208  addnidpig  7420  frecfzennn  10535  hashinfom  10887  hashennn  10889  hashp1i  10919  ennnfonelemg  12645  ctinfom  12670