Theorem ordirr 6231

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2110   E cep 5459   Fr wfr 5506  Ord word 6212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-eprel 5460  df-fr 5509  df-we 5511  df-ord 6216

This theorem is referenced by:  nordeq  6232  ordn2lp  6233  ordtri3or  6245  ordtri1  6246  ordtri3  6249  orddisj  6251  ordunidif  6261  ordnbtwn  6303  onirri  6320  onssneli  6323  onprc  7562  nlimsucg  7621  nnlim  7658  limom  7660  smo11  8101  smoord  8102  tfrlem13  8126  omopth2  8312  limensuci  8822  infensuc  8824  ordtypelem9  9142  cantnfp1lem3  9295  cantnfp1  9296  oemapvali  9299  tskwe  9566  dif1card  9624  dju1p1e2ALT  9788  nnadju  9811  pwsdompw  9818  cflim2  9877  fin23lem24  9936  fin23lem26  9939  axdc3lem4  10067  ttukeylem7  10129  canthp1lem2  10267  inar1  10389  gruina  10432  grur1  10434  addnidpi  10515  fzennn  13541  hashp1i  13970  soseq  33540  naddcllem  33568  noseponlem  33604  noextend  33606  noextenddif  33608  noextendlt  33609  noextendgt  33610  fvnobday  33618  nosepssdm  33626  nosupbnd1lem3  33650  nosupbnd1lem5  33652  nosupbnd2lem1  33655  noinfbnd1lem3  33665  noinfbnd1lem5  33667  noinfbnd2lem1  33670  noetasuplem4  33676  noetainflem4  33680  sucneqond  35273