Theorem ordirr 6269

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   E cep 5485   Fr wfr 5532  Ord word 6250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-eprel 5486  df-fr 5535  df-we 5537  df-ord 6254

This theorem is referenced by:  nordeq  6270  ordn2lp  6271  ordtri3or  6283  ordtri1  6284  ordtri3  6287  orddisj  6289  ordunidif  6299  ordnbtwn  6341  onirri  6358  onssneli  6361  onprc  7605  nlimsucg  7664  nnlim  7701  limom  7703  smo11  8166  smoord  8167  tfrlem13  8192  omopth2  8377  limensuci  8889  infensuc  8891  ordtypelem9  9215  cantnfp1lem3  9368  cantnfp1  9369  oemapvali  9372  tskwe  9639  dif1card  9697  dju1p1e2ALT  9861  nnadju  9884  pwsdompw  9891  cflim2  9950  fin23lem24  10009  fin23lem26  10012  axdc3lem4  10140  ttukeylem7  10202  canthp1lem2  10340  inar1  10462  gruina  10505  grur1  10507  addnidpi  10588  fzennn  13616  hashp1i  14046  soseq  33730  naddcllem  33758  noseponlem  33794  noextend  33796  noextenddif  33798  noextendlt  33799  noextendgt  33800  fvnobday  33808  nosepssdm  33816  nosupbnd1lem3  33840  nosupbnd1lem5  33842  nosupbnd2lem1  33845  noinfbnd1lem3  33855  noinfbnd1lem5  33857  noinfbnd2lem1  33860  noetasuplem4  33866  noetainflem4  33870  sucneqond  35463