Theorem ordirr 6208

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2110   E cep 5463   Fr wfr 5510  Ord word 6189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-br 5066  df-opab 5128  df-eprel 5464  df-fr 5513  df-we 5515  df-ord 6193

This theorem is referenced by:  nordeq  6209  ordn2lp  6210  ordtri3or  6222  ordtri1  6223  ordtri3  6226  orddisj  6228  ordunidif  6238  ordnbtwn  6280  onirri  6296  onssneli  6299  onprc  7498  nlimsucg  7556  nnlim  7592  limom  7594  smo11  8000  smoord  8001  tfrlem13  8025  omopth2  8209  limensuci  8692  infensuc  8694  ordtypelem9  8989  cantnfp1lem3  9142  cantnfp1  9143  oemapvali  9146  tskwe  9378  dif1card  9435  dju1p1e2ALT  9599  pwsdompw  9625  cflim2  9684  fin23lem24  9743  fin23lem26  9746  axdc3lem4  9874  ttukeylem7  9936  canthp1lem2  10074  inar1  10196  gruina  10239  grur1  10241  addnidpi  10322  fzennn  13335  hashp1i  13763  soseq  33096  noseponlem  33171  noextend  33173  noextenddif  33175  noextendlt  33176  noextendgt  33177  fvnobday  33183  nosepssdm  33190  nosupbnd1lem3  33210  nosupbnd1lem5  33212  nosupbnd2lem1  33215  noetalem3  33219  sucneqond  34645