Theorem ordirr 5965

Description: Epsilon irreflexivity of ordinals: no ordinal class is a member of itself. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. 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 5962	. 2 ⊢ (Ord 𝐴 → E Fr 𝐴)
2		efrirr 5303	. 2 ⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴)
3	1, 2	syl 17	1 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2157   E cep 5234   Fr wfr 5278  Ord word 5946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4986  ax-nul 4994  ax-pr 5107

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-sbc 3645  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-br 4856  df-opab 4918  df-eprel 5235  df-fr 5281  df-we 5283  df-ord 5950

This theorem is referenced by:  nordeq  5966  ordn2lp  5967  ordtri3or  5979  ordtri1  5980  ordtri3  5983  orddisj  5985  ordunidif  5996  ordnbtwn  6038  onirri  6054  onssneli  6057  onprc  7221  nlimsucg  7279  nnlim  7315  limom  7317  smo11  7704  smoord  7705  tfrlem13  7729  omopth2  7908  limensuci  8382  infensuc  8384  ordtypelem9  8677  cantnfp1lem3  8831  cantnfp1  8832  oemapvali  8835  tskwe  9066  dif1card  9123  pm110.643ALT  9292  pwsdompw  9318  cflim2  9377  fin23lem24  9436  fin23lem26  9439  axdc3lem4  9567  ttukeylem7  9629  canthp1lem2  9767  inar1  9889  gruina  9932  grur1  9934  addnidpi  10015  fzennn  12998  hashp1i  13415  soseq  32084  noseponlem  32147  noextend  32149  noextenddif  32151  noextendlt  32152  noextendgt  32153  fvnobday  32159  nosepssdm  32166  nosupbnd1lem3  32186  nosupbnd1lem5  32188  nosupbnd2lem1  32191  noetalem3  32195  sucneqond  33535