Theorem ordirr 4595

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

Assertion

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

Proof of Theorem ordirr

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2177  Ord word 4414

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-setind 4590

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-ral 2490  df-v 2775  df-dif 3170  df-sn 3641

This theorem is referenced by:  onirri  4596  nordeq  4597  ordn2lp  4598  orddisj  4599  onprc  4605  nlimsucg  4619  tfr1onlemsucfn  6436  tfr1onlemsucaccv  6437  tfrcllemsucfn  6449  tfrcllemsucaccv  6450  nntr2  6599  unsnfi  7028  nnnninfeq  7242  nninfisol  7247  addnidpig  7462  frecfzennn  10584  hashinfom  10936  hashennn  10938  hashp1i  10968  ennnfonelemg  12824  ctinfom  12849