Theorem ordirr 5741

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 1990   E cep 5028   Fr wfr 5070  Ord word 5722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-eprel 5029  df-fr 5073  df-we 5075  df-ord 5726

This theorem is referenced by:  nordeq  5742  ordn2lp  5743  ordtri3or  5755  ordtri1  5756  ordtri3  5759  ordtri3OLD  5760  orddisj  5762  ordunidif  5773  ordnbtwn  5816  ordnbtwnOLD  5817  onirri  5834  onssneli  5837  onprc  6984  nlimsucg  7042  nnlim  7078  limom  7080  smo11  7461  smoord  7462  tfrlem13  7486  omopth2  7664  limensuci  8136  infensuc  8138  ordtypelem9  8431  cantnfp1lem3  8577  cantnfp1  8578  oemapvali  8581  tskwe  8776  dif1card  8833  pm110.643ALT  9000  pwsdompw  9026  cflim2  9085  fin23lem24  9144  fin23lem26  9147  axdc3lem4  9275  ttukeylem7  9337  canthp1lem2  9475  inar1  9597  gruina  9640  grur1  9642  addnidpi  9723  fzennn  12767  hashp1i  13191  soseq  31751  noseponlem  31817  noextend  31819  noextenddif  31821  noextendlt  31822  noextendgt  31823  fvnobday  31829  nosepssdm  31836  nosupbnd1lem3  31856  nosupbnd1lem5  31858  nosupbnd2lem1  31861  noetalem3  31865  sucneqond  33213