Theorem ordirr 6209

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   E cep 5464   Fr wfr 5511  Ord word 6190

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  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 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-eprel 5465  df-fr 5514  df-we 5516  df-ord 6194

This theorem is referenced by:  nordeq  6210  ordn2lp  6211  ordtri3or  6223  ordtri1  6224  ordtri3  6227  orddisj  6229  ordunidif  6239  ordnbtwn  6281  onirri  6297  onssneli  6300  onprc  7499  nlimsucg  7557  nnlim  7593  limom  7595  smo11  8001  smoord  8002  tfrlem13  8026  omopth2  8210  limensuci  8693  infensuc  8695  ordtypelem9  8990  cantnfp1lem3  9143  cantnfp1  9144  oemapvali  9147  tskwe  9379  dif1card  9436  dju1p1e2ALT  9600  pwsdompw  9626  cflim2  9685  fin23lem24  9744  fin23lem26  9747  axdc3lem4  9875  ttukeylem7  9937  canthp1lem2  10075  inar1  10197  gruina  10240  grur1  10242  addnidpi  10323  fzennn  13337  hashp1i  13765  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  34649