Theorem ordirr 6047

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2050   E cep 5316   Fr wfr 5363  Ord word 6028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pr 5186

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3682  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-br 4930  df-opab 4992  df-eprel 5317  df-fr 5366  df-we 5368  df-ord 6032

This theorem is referenced by:  nordeq  6048  ordn2lp  6049  ordtri3or  6061  ordtri1  6062  ordtri3  6065  orddisj  6067  ordunidif  6077  ordnbtwn  6119  onirri  6135  onssneli  6138  onprc  7315  nlimsucg  7373  nnlim  7409  limom  7411  smo11  7805  smoord  7806  tfrlem13  7830  omopth2  8011  limensuci  8489  infensuc  8491  ordtypelem9  8785  cantnfp1lem3  8937  cantnfp1  8938  oemapvali  8941  tskwe  9173  dif1card  9230  dju1p1e2ALT  9398  pwsdompw  9424  cflim2  9483  fin23lem24  9542  fin23lem26  9545  axdc3lem4  9673  ttukeylem7  9735  canthp1lem2  9873  inar1  9995  gruina  10038  grur1  10040  addnidpi  10121  fzennn  13151  hashp1i  13577  soseq  32623  noseponlem  32698  noextend  32700  noextenddif  32702  noextendlt  32703  noextendgt  32704  fvnobday  32710  nosepssdm  32717  nosupbnd1lem3  32737  nosupbnd1lem5  32739  nosupbnd2lem1  32742  noetalem3  32746  sucneqond  34094