Theorem ordirr 5884

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2145   E cep 5161   Fr wfr 5205  Ord word 5865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-br 4787  df-opab 4847  df-eprel 5162  df-fr 5208  df-we 5210  df-ord 5869

This theorem is referenced by:  nordeq  5885  ordn2lp  5886  ordtri3or  5898  ordtri1  5899  ordtri3  5902  ordtri3OLD  5903  orddisj  5905  ordunidif  5916  ordnbtwn  5959  ordnbtwnOLD  5960  onirri  5977  onssneli  5980  onprc  7131  nlimsucg  7189  nnlim  7225  limom  7227  smo11  7614  smoord  7615  tfrlem13  7639  omopth2  7818  limensuci  8292  infensuc  8294  ordtypelem9  8587  cantnfp1lem3  8741  cantnfp1  8742  oemapvali  8745  tskwe  8976  dif1card  9033  pm110.643ALT  9202  pwsdompw  9228  cflim2  9287  fin23lem24  9346  fin23lem26  9349  axdc3lem4  9477  ttukeylem7  9539  canthp1lem2  9677  inar1  9799  gruina  9842  grur1  9844  addnidpi  9925  fzennn  12975  hashp1i  13393  soseq  32091  noseponlem  32154  noextend  32156  noextenddif  32158  noextendlt  32159  noextendgt  32160  fvnobday  32166  nosepssdm  32173  nosupbnd1lem3  32193  nosupbnd1lem5  32195  nosupbnd2lem1  32198  noetalem3  32202  sucneqond  33550