eloni - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > eloni		Structured version Visualization version GIF version

Theorem eloni 6374

Description: An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)

**Assertion**
Ref	Expression
eloni	⊢ (𝐴 ∈ On → Ord 𝐴)

**Proof of Theorem eloni**
Step	Hyp	Ref	Expression
1		elong 6372	. 2 ⊢ (𝐴 ∈ On → (𝐴 ∈ On ↔ Ord 𝐴))
2	1	ibi 267	1 ⊢ (𝐴 ∈ On → Ord 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2099 Ord word 6363 Oncon0 6364

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699

This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3058 df-v 3472 df-in 3952 df-ss 3962 df-uni 4905 df-tr 5261 df-po 5585 df-so 5586 df-fr 5628 df-we 5630 df-ord 6367 df-on 6368

This theorem is referenced by: onelon 6389 onin 6395 ontri1 6398 onfr 6403 onelpss 6404 onsseleq 6405 onelss 6406 ontr1 6410 ontr2 6411 ordunidif 6413 on0eln0 6420 ordsssuc 6453 onsssuc 6454 onnbtwn 6458 onunel 6469 suc11 6471 onun2 6472 ontr 6473 onordi 6475 onssneli 6480 epweon 7772 epweonALT 7773 ordeleqon 7779 onss 7782 sucexeloni 7807 ordsucOLD 7812 onpwsuc 7814 onpsssuc 7817 onsucmin 7819 ordunpr 7824 ordunisuc 7830 onsucuni2 7832 onuniorsuc 7835 ordunisuc2 7843 ordzsl 7844 onzsl 7845 nlimon 7850 tfinds 7859 tfindsg2 7861 nnord 7873 poseq 8158 soseq 8159 onfununi 8356 smo11 8379 smoord 8380 smoword 8381 smogt 8382 tfrlem1 8391 tfrlem9a 8401 tfrlem15 8407 tz7.44-2 8422 tz7.48lem 8456 ord3 8498 oe0m1 8536 oaordi 8561 oaord 8562 oacan 8563 oawordri 8565 oalimcl 8575 oaass 8576 omord2 8582 omcan 8584 omwordi 8586 omword1 8588 omword2 8589 om00 8590 omlimcl 8593 omass 8595 omeulem2 8598 omopth2 8599 oen0 8601 oeord 8603 oecan 8604 oewordi 8606 oeworde 8608 oelimcl 8615 oeeulem 8616 oeeui 8617 nnarcl 8631 nnawordi 8636 nnawordex 8652 oaabs2 8664 omabs 8666 omsmo 8673 cofonr 8689 naddcllem 8691 omxpenlem 9092 infensuc 9174 dif1enlem 9175 nndomog 9235 nndomogOLD 9245 onomeneq 9247 onomeneqOLD 9248 ordiso 9534 ordtypelem2 9537 hartogslem1 9560 cantnflt 9690 cantnfp1lem3 9698 cantnfp1 9699 oemapso 9700 oemapvali 9702 cantnflem1d 9706 cantnflem1 9707 cantnf 9711 oemapwe 9712 cantnffval2 9713 cnfcom 9718 r111 9793 r1ordg 9796 rankonidlem 9846 bndrank 9859 r1pw 9863 r1pwALT 9864 rankbnd2 9887 tcrank 9902 cardprclem 9997 carduni 9999 cardmin2 10017 infxpenlem 10031 alephdom 10099 alephdom2 10105 cardaleph 10107 iscard3 10111 alephfp 10126 dfac12lem1 10161 dfac12lem2 10162 dfac12lem3 10163 cflim2 10281 cofsmo 10287 cfsmolem 10288 coftr 10291 cfcof 10292 fin67 10413 hsmexlem5 10448 zorn2lem6 10519 ttukeylem3 10529 ttukeylem5 10531 ttukeylem6 10532 ttukeylem7 10533 winainflem 10711 r1limwun 10754 r1wunlim 10755 tsksuc 10780 inar1 10793 gruina 10836 grur1a 10837 grur1 10838 nodmord 27580 noextendseq 27594 noextenddif 27595 nosupno 27630 nosupbday 27632 nosupres 27634 noinfno 27645 noinfbday 27647 noinfres 27649 noetasuplem4 27663 noetainflem4 27667 newbday 27822 dfrdg2 35386 ontgval 35910 ontgsucval 35911 onsuctopon 35913 onintopssconn 35919 onsuct0 35920 sucneqond 36839 onsucuni3 36841 aomclem4 42472 aomclem5 42473 onintunirab 42646 omlimcl2 42661 onelord 42670 oneltri 42677 ordeldifsucon 42679 ordeldif1o 42680 onsucss 42686 onsucf1olem 42690 onov0suclim 42694 oe0rif 42705 onsucwordi 42708 oege1 42726 cantnfresb 42744 omabs2 42752 ordsssucb 42755 tfsconcatlem 42756 tfsconcatfv2 42760 tfsconcatrn 42762 tfsconcatb0 42764 tfsconcat0b 42766 tfsconcatrev 42768 onsucunipr 42792 oaun3lem1 42794 oaun3lem2 42795 nadd1suc 42812 naddsuc2 42813 naddgeoa 42815 oaltom 42826 omltoe 42828 nlimsuc 42862 dfsucon 42944 minregex 42955 onfrALTlem3 43974 onfrALTlem2 43976 onfrALTlem3VD 44317 onfrALTlem2VD 44319 onsetreclem3 48129

Copyright terms: Public domain

	
		OSZAR »