mmtheorems39 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 3801-3900 - Page 39 of 175

Type	Label	Description
Statement
Theorem	snnex 3801	The class of all singletons is a proper class. (Proof shortened by Eric Schmidt, 7-Dec-2008.)
|- {x | E.y x = {y}} e/ _V
Theorem	difex2 3802	If the subtrahend of a class difference exists, then the minuend exists iff the difference exists. (The proof was shortened by Andrew Salmon, 12-Aug-2011.)
|- (B e. C -> (A e. _V <-> (A \ B) e. _V))
Theorem	difex2OLD 3803	If the subtrahend of a class difference exists, then the minuend exists iff the difference exists.
|- (B e. C -> (A e. _V <-> (A \ B) e. _V))
Theorem	tpex 3804	A triple of classes exists.
|- {A, B, C} e. _V
Theorem	opeluu 3805	Each member of an ordered pair belongs to the union of the union of a class to which the ordered pair belongs. Lemma 3D of [Enderton] p. 41.
|- (<.x, y>. e. A -> (x e. U.U.A /\ y e. U.U.A))
Theorem	uniuni 3806	Expression for double union that moves union into a class builder. (Contributed by FL, 28-May-2007.)
|- U.U.A = U.{x | E.y(x = U.y /\ y e. A)}
Theorem	euuni 3807	If ph is true for exactly one x, then U.{x | ph} is a way to express "the unique element such that ph is true." Some books use a special symbol such as iota to denote "the unique element such that."
|- (E!xph -> (ph <-> U.{x | ph} = x))
Theorem	reuuni1 3808	A way to express "the unique element such that" (restricted quantifier version). (The proof was shortened by Andrew Salmon, 12-Aug-2011.)
|- ((x e. A /\ E!x e. A ph) -> (ph <-> U.{x e. A | ph} = x))
Theorem	reuuni1OLD 3809	A way to express "the unique element such that" (restricted quantifier version).
|- ((x e. A /\ E!x e. A ph) -> (ph <-> U.{x e. A | ph} = x))
Theorem	reuuni2f 3810	U.{x e. A | ph} is an explicit representation of "the unique element in A such that ph." This theorem shows a condition that allows us to represent this element with a class expression B. The second hypothesis is a weakened bound variable condition that allows hbsbc1g 2461 to be used.
|- (y e. B -> A.x y e. B)   &   |- (B e. A -> (ps -> A.xps))   &   |- (x = B -> (ph <-> ps))   =>   |- ((B e. A /\ E!x e. A ph) -> (ps <-> U.{x e. A | ph} = B))
Theorem	reuuni2 3811	U.{x e. A | ph} is an explicit representation of "the unique element in A such that ph."
|- (x = B -> (ph <-> ps))   =>   |- ((B e. A /\ E!x e. A ph) -> (ps <-> U.{x e. A | ph} = B))
Theorem	reuuni3 3812	Derive the property ch of "the unique element in A such that ph " when expressed explicitly as U.{y e. A | ps}.
|- (x = y -> (ph <-> ps))   &   |- (x = U.{y e. A | ps} -> (ph <-> ch))   =>   |- (E!x e. A ph -> ch)
Theorem	reuuni4 3813	Derive the property of "the unique element in A such that ph " when expressed explicitly as U.{x e. A | ph}.
|- (E!x e. A ph -> [U.{x e. A | ph} / x]ph)
Theorem	reucl2 3814	Membership law for "the unique element in A such that ph."
|- (E!x e. A ph -> U.{x e. A | ph} e. {x e. A | ph})
Theorem	reuuniss 3815	Restriction of a unique element to a smaller class.
|- ((A C_ B /\ E.x e. A ph /\ E!x e. B ph) -> U.{x e. A | ph} = U.{x e. B | ph})
Theorem	mouniss 3816	Restriction of a unique element to a smaller class.
|- ((A C_ B /\ E.x e. A ph /\ E*x(x e. B /\ ph)) -> U.{x e. A | ph} = U.{x e. B | ph})
Theorem	reuuniss2 3817	Restriction of a unique element to a smaller class.
|- (((A C_ B /\ A.x e. A (ph -> ps)) /\ (E.x e. A ph /\ E!x e. B ps)) -> U.{x e. A | ph} = U.{x e. B | ps})
Theorem	reusn 3818	A way to express restricted existential uniqueness of a wff: its restricted class abstraction is a singleton. (The proof was shortened by Andrew Salmon, 12-Aug-2011.)
|- (E!x e. A ph <-> E.y{x e. A | ph} = {y})
Theorem	reusnOLD 3819	A way to express restricted existential uniqueness of a wff: its restricted class abstraction is a singleton.
|- (E!x e. A ph <-> E.y{x e. A | ph} = {y})
Theorem	reusni 3820	Restricted existential uniqueness determined by a singleton.
|- B e. _V   =>   |- ({x e. A | ph} = {B} -> E!x e. A ph)
Theorem	rabsnt 3821	Truth implied by equality of a restricted class abstraction and a singleton.
|- B e. _V   &   |- (x = B -> (ph <-> ps))   =>   |- ({x e. A | ph} = {B} -> ps)
Theorem	reuunisn 3822	A restricted class abstraction with a unique member can be expressed as a singleton.
|- (E!x e. A ph -> {x e. A | ph} = {U.{x e. A | ph}})
Theorem	eualeq 3823	Two ways to express single-valuedness of a class expression A(x).
|- (E!yA.x y = A <-> E.yA.x y = A)
Theorem	eualeqhb 3824	Even if x is free in A, it is effectively bound when A(x) is single-valued.
|- (E!yA.x y = A -> (y = A -> A.x y = A))
Theorem	eualexeq 3825	Two ways to express single-valuedness of a class expression A(x).
|- (E!yA.x y = A -> E!yE.x y = A)
Theorem	euexeqOLD 3826	Two ways to express single-valuedness of a class expression A(x).
|- A e. _V   =>   |- (E!yE.x y = A <-> E!yA.x y = A)
Theorem	euexaleq 3827	Two ways to express single-valuedness of a class expression A(x).
|- A e. _V   =>   |- (E!yE.x y = A <-> E!yA.x y = A)
Theorem	eufromeq1 3828	Two ways of expressing existential uniqueness via an indirect equality.
|- (A =/= (/) -> (E!xA.y e. A x = B <-> E.xA.y e. A x = B))
Theorem	eufromeq2 3829	Two ways of expressing existential uniqueness via an indirect equality.
|- (E!xA.y e. A x = B -> E!xE.y e. A x = B)
Theorem	eufromeq3 3830	Two ways of expressing existential uniqueness via an indirect equality.
|- B e. _V   =>   |- (E!xE.y e. A x = B <-> E!xA.y e. A x = B)
Theorem	eufromeq4 3831	Two ways of expressing existential uniqueness via an indirect equality. This shows eufromeq3 3830 in a more general-looking form.
|- C e. _V   =>   |- (E!x e. A E.y e. B (ph /\ x = C) <-> E!xA.y e. B ((C e. A /\ ph) -> x = C))
Theorem	eufromeq5 3832	Two ways of expressing existential uniqueness via an indirect equality.
|- (B =/= (/) -> (E!x e. A A.y e. B x = C <-> E.x e. A A.y e. B x = C))
Theorem	eufromeq6 3833	Two ways of expressing existential uniqueness via an indirect equality. The converse does not hold. Note that U.A = |^|A means A is a singleton (uniintsn 3253).
|- ((U.A =/= |^|A \/ B =/= (/)) -> (E!x e. A A.y e. B x = C -> E!x e. A E.y e. B x = C))
Theorem	euobj1 3834	The two existential uniqueness expressions of eufromeq3 3830 specify the same object.
|- B e. _V   =>   |- (E!xE.y e. A x = B -> U.{x | E.y e. A x = B} = U.{x | A.y e. A x = B})
Theorem	euobj2 3835	The two existential uniqueness expressions of eufromeq3 3830 specify the same property.
|- B e. _V   =>   |- (E!xE.y e. A x = B -> (E.y e. A x = B <-> A.y e. A x = B))
Theorem	alxfr 3836	Transfer universal quantification from a variable x to another variable y contained in expression A.
|- (x = A -> (ph <-> ps))   =>   |- ((A.y A e. B /\ A.xE.y x = A) -> (A.xph <-> A.yps))
Theorem	ralxfrd 3837	Transfer universal quantification from a variable x to another variable y contained in expression A.
|- ((ph /\ y e. B) -> A e. B)   &   |- ((ph /\ x e. B) -> E.y e. B x = A)   &   |- ((ph /\ x = A) -> (ps <-> ch))   =>   |- (ph -> (A.x e. B ps <-> A.y e. B ch))
Theorem	rexxfrd 3838	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by FL, 10-Apr-2007.)
|- ((ph /\ y e. B) -> A e. B)   &   |- ((ph /\ x e. B) -> E.y e. B x = A)   &   |- ((ph /\ x = A) -> (ps <-> ch))   =>   |- (ph -> (E.x e. B ps <-> E.y e. B ch))
Theorem	ralxfr 3839	Transfer universal quantification from a variable x to another variable y contained in expression A.
|- (y e. B -> A e. B)   &   |- (x e. B -> E.y e. B x = A)   &   |- (x = A -> (ph <-> ps))   =>   |- (A.x e. B ph <-> A.y e. B ps)
Theorem	ralxfrALT 3840	Transfer universal quantification from a variable x to another variable y contained in expression A.
|- (y e. B -> A e. B)   &   |- (x e. B -> E.y e. B x = A)   &   |- (x = A -> (ph <-> ps))   =>   |- (A.x e. B ph <-> A.y e. B ps)
Theorem	rexxfr 3841	Transfer existence from a variable x to another variable y contained in expression A.
|- (y e. B -> A e. B)   &   |- (x e. B -> E.y e. B x = A)   &   |- (x = A -> (ph <-> ps))   =>   |- (E.x e. B ph <-> E.y e. B ps)
Theorem	rabxfrd 3842	Class builder membership after substituting an expression A (containing y) for x in the class expression ch.
|- (z e. B -> A.y z e. B)   &   |- (z e. C -> A.y z e. C)   &   |- ((ph /\ y e. D) -> A e. D)   &   |- (x = A -> (ps <-> ch))   &   |- (y = B -> A = C)   =>   |- ((ph /\ B e. D) -> (C e. {x e. D | ps} <-> B e. {y e. D | ch}))
Theorem	rabxfr 3843	Class builder membership after substituting an expression A (containing y) for x in the class expression ph.
|- (z e. B -> A.y z e. B)   &   |- (z e. C -> A.y z e. C)   &   |- (y e. D -> A e. D)   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> A = C)   =>   |- (B e. D -> (C e. {x e. D | ph} <-> B e. {y e. D | ps}))
Theorem	reuxfr2d 3844	Transfer existential uniqueness from a variable x to another variable y contained in expression A.
|- ((ph /\ y e. B) -> A e. B)   &   |- ((ph /\ x e. B) -> E*y(y e. B /\ x = A))   =>   |- (ph -> (E!x e. B E.y e. B (x = A /\ ps) <-> E!y e. B ps))
Theorem	reuxfr2 3845	Transfer existential uniqueness from a variable x to another variable y contained in expression A.
|- (y e. B -> A e. B)   &   |- (x e. B -> E*y(y e. B /\ x = A))   =>   |- (E!x e. B E.y e. B (x = A /\ ph) <-> E!y e. B ph)
Theorem	reuxfrd 3846	Transfer existential uniqueness from a variable x to another variable y contained in expression A. Use reuhypd 3848 to eliminate the second hypothesis.
|- ((ph /\ y e. B) -> A e. B)   &   |- ((ph /\ x e. B) -> E!y e. B x = A)   &   |- (x = A -> (ps <-> ch))   =>   |- (ph -> (E!x e. B ps <-> E!y e. B ch))
Theorem	reuxfr 3847	Transfer existential uniqueness from a variable x to another variable y contained in expression A. Use reuhyp 3849 to eliminate the second hypothesis.
|- (y e. B -> A e. B)   &   |- (x e. B -> E!y e. B x = A)   &   |- (x = A -> (ph <-> ps))   =>   |- (E!x e. B ph <-> E!y e. B ps)
Theorem	reuhypd 3848	A theorem useful for eliminating the restricted existential uniqueness hypotheses in riotaxfrd 5581.
|- ((ph /\ x e. C) -> B e. C)   &   |- ((ph /\ x e. C /\ y e. C) -> (x = A <-> y = B))   =>   |- ((ph /\ x e. C) -> E!y e. C x = A)
Theorem	reuhyp 3849	A theorem useful for eliminating the restricted existential uniqueness hypotheses in reuxfr 3847.
|- (x e. C -> B e. C)   &   |- ((x e. C /\ y e. C) -> (x = A <-> y = B))   =>   |- (x e. C -> E!y e. C x = A)
Theorem	reuunixfr 3850	Change the variable x in the expression for "the unique A such that ph " to another variable y contained in expression B. Use reuhyp 3849 to eliminate the last hypothesis.
|- (z e. C -> A.y z e. C)   &   |- (y e. A -> B e. A)   &   |- (U.{y e. A | ps} e. A -> C e. A)   &   |- (x = B -> (ph <-> ps))   &   |- (y = U.{y e. A | ps} -> B = C)   &   |- (x e. A -> E!y e. A x = B)   =>   |- (E!x e. A ph -> U.{x e. A | ph} = C)
Theorem	uniexb 3851	The Axiom of Union and its converse. A class is a set iff its union is a set.
|- (A e. _V <-> U.A e. _V)
Theorem	pwexb 3852	The Axiom of Power Sets and its converse. A class is a set iff its power class is a set.
|- (A e. _V <-> ~PA e. _V)
Theorem	univ 3853	The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235.
|- U._V = _V
Theorem	eldifpw 3854	Membership in a power class difference.
|- C e. _V   =>   |- ((A e. ~PB /\ -. C C_ B) -> (A u. C) e. (~P(B u. C) \ ~PB))
Theorem	elpwun 3855	Membership in the power class of a union.
|- C e. _V   =>   |- (A e. ~P(B u. C) <-> (A \ C) e. ~PB)
Theorem	elpwunsn 3856	Membership in an extension of a power class.
|- (A e. (~P(B u. {C}) \ ~PB) -> C e. A)
Theorem	op1stb 3857	Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (See op2ndb 4376 to extract the second member, op1sta 4372 for an alternate version, and op1st 5026 for the preferred version.)
|- A e. _V   =>   |- |^||^|<.A, B>. = A
Theorem	iunpw 3858	An indexed union of a power class in terms of the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33.
|- A e. _V   =>   |- (E.x e. A x = U.A <-> ~PU.A = U_x e. A ~Px)
Theorem	fr3nr 3859	A founded relation has no 3-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30.
|- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. (xRy /\ yRz /\ zRx))
Theorem	epne3 3860	A set founded by epsilon contains no 3-cycle loops.
|- (( _E Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. (x e. y /\ y e. z /\ z e. x))
Theorem	dfwe2 3861	Alternate definition of well-ordering. Definition 6.24(2) of [TakeutiZaring] p. 30. (The proof was shortened by Andrew Salmon, 12-Aug-2011.)
|- (R We A <-> (R Fr A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
Theorem	dfwe2OLD 3862	Alternate definition of well-ordering. Definition 6.24(2) of [TakeutiZaring] p. 30.
|- (R We A <-> (R Fr A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
Ordinals (continued)
Theorem	ordon 3863	The class of all ordinal numbers is ordinal. Proposition 7.12 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity.
|- Ord On
Theorem	epweon 3864	The epsilon relation well-orders the class of ordinal numbers. Proposition 4.8(g) of [Mendelson] p. 244.
|- _E We On
Theorem	onprc 3865	No set contains all ordinal numbers. Proposition 7.13 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. This is also known as the Burali-Forti paradox (remark in [Enderton] p. 194). In 1897, Cesare Burali-Forti noticed that since the "set" of all ordinal numbers is an ordinal class (ordon 3863), it must be both an element of the set of all ordinal numbers yet greater than every such element. ZF set theory resolves this paradox by not allowing the class of all ordinal numbers to be a set (so instead it is a proper class). Here we prove the denial of its existence.
|- -. On e. _V
Theorem	ordeleqon 3866	A way to express the ordinal property of a class in terms of the class of ordinal numbers. Corollary 7.14 of [TakeutiZaring] p. 38 and its converse.
|- (Ord A <-> (A e. On \/ A = On))
Theorem	ordsson 3867	Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38. (The proof was shortened by Andrew Salmon, 12-Aug-2011.)
|- (Ord A -> A C_ On)
Theorem	ordssonOLD 3868	Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38.
|- (Ord A -> A C_ On)
Theorem	onss 3869	An ordinal number is a subset of the class of ordinal numbers.
|- (A e. On -> A C_ On)
Theorem	ssorduni 3870	The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40. (The proof was shortened by Andrew Salmon, 12-Aug-2011.)
|- (A C_ On -> Ord U.A)
Theorem	ssorduniOLD 3871	The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40.
|- (A C_ On -> Ord U.A)
Theorem	ssonuni 3872	The union of a set of ordinal numbers is an ordinal number. Theorem 9 of [Suppes] p. 132.
|- (A e. B -> (A C_ On -> U.A e. On))
Theorem	ssonunii 3873	The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of [Enderton] p. 193.
|- A e. _V   =>   |- (A C_ On -> U.A e. On)
Theorem	onuni 3874	The union of an ordinal number is an ordinal number.
|- (A e. On -> U.A e. On)
Theorem	orduni 3875	The union of an ordinal class is ordinal.
|- (Ord A -> Ord U.A)
Theorem	onint 3876	The intersection (infimum) of a non-empty class of ordinal numbers belongs to the class. Compare Exercise 4 of [TakeutiZaring] p. 45.
|- ((A C_ On /\ A =/= (/)) -> |^|A e. A)
Theorem	onint0 3877	The intersection of a class of ordinal numbers is zero iff the class contains zero.
|- (A C_ On -> (|^|A = (/) <-> (/) e. A))
Theorem	onssmin 3878	A non-empty class of ordinal numbers has a smallest member. Exercise 9 of [TakeutiZaring] p. 40.
|- ((A C_ On /\ A =/= (/)) -> E.x e. A A.y e. A x C_ y)
Theorem	onminsb 3879	If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses implicit substitution. Theorem Schema 62 of [Suppes] p. 228.
|- (ps -> A.xps)   &   |- (x = |^|{x e. On | ph} -> (ph <-> ps))   =>   |- (E.x e. On ph -> ps)
Theorem	onminesb 3880	If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses explicit substitution. Theorem Schema 62 of [Suppes] p. 228.
|- (E.x e. On ph -> [|^|{x e. On | ph} / x]ph)
Theorem	oninton 3881	The intersection of a non-empty collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44.
|- ((A C_ On /\ A =/= (/)) -> |^|A e. On)
Theorem	onintrab 3882	The intersection of a class of ordinal numbers exists iff it is an ordinal number.
|- (|^|{x e. On | ph} e. _V <-> |^|{x e. On | ph} e. On)
Theorem	onintrab2 3883	An existence condition equivalent to an intersection's being an ordinal number.
|- (E.x e. On ph <-> |^|{x e. On | ph} e. On)
Theorem	onnmin 3884	No member of a set of ordinal numbers belongs to its minimum.
|- ((A C_ On /\ B e. A) -> -. B e. |^|A)
Theorem	onnminsb 3885	An ordinal number smaller than the minimum of a set of ordinal numbers does not have the property determining that set. ps is the wff resulting from the substitution of A for x in wff ph.
|- (x = A -> (ph <-> ps))   =>   |- (A e. On -> (A e. |^|{x e. On | ph} -> -. ps))
Theorem	oneqmin 3886	A way to show that an ordinal number equals the minimum of a non-empty collection of ordinal numbers: it must be in the collection, and it must not be larger than any member of the collection.
|- ((B C_ On /\ B =/= (/)) -> (A = |^|B <-> (A e. B /\ A.x e. A -. x e. B)))
Theorem	bm2.5ii 3887	Problem 2.5(ii) of [BellMachover] p. 471.
|- A e. _V   =>   |- (A C_ On -> U.A = |^|{x e. On | A.y e. A y C_ x})
Theorem	onminex 3888	If a wff is true for an ordinal number, there is a smallest ordinal number for which it is true.
|- (x = y -> (ph <-> ps))   =>   |- (E.x e. On ph -> E.x e. On (ph /\ A.y e. x -. ps))
Theorem	sucon 3889	The class of all ordinal numbers is its own successor.
|- suc On = On
Theorem	sucexb 3890	A successor exists iff its class argument exists.
|- (A e. _V <-> suc A e. _V)
Theorem	sucexg 3891	The successor of a set is a set (generalization).
|- (A e. B -> suc A e. _V)
Theorem	sucex 3892	The successor of a set is a set.
|- A e. _V   =>   |- suc A e. _V
Theorem	onmindif2 3893	The minimum of a class of ordinal numbers is less than the minimum of that class with its minimum removed.
|- ((A C_ On /\ A =/= (/)) -> |^|A e. |^|(A \ {|^|A}))
Theorem	suceloni 3894	The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41.
|- (A e. On -> suc A e. On)
Theorem	ordsuc 3895	The successor of an ordinal class is ordinal.
|- (Ord A <-> Ord suc A)
Theorem	ordpwsuc 3896	The collection of ordinals in the power class of an ordinal is its successor.
|- (Ord A -> (~PA i^i On) = suc A)
Theorem	onpwsuc 3897	The collection of ordinal numbers in the power set of an ordinal number is its successor.
|- (A e. On -> (~PA i^i On) = suc A)
Theorem	sucelon 3898	The successor of an ordinal number is an ordinal number.
|- (A e. On <-> suc A e. On)
Theorem	ordsucss 3899	The successor of an element of an ordinal class is a subset of it.
|- (Ord B -> (A e. B -> suc A C_ B))
Theorem	ordelsuc 3900	A set belongs to an ordinal iff its successor is a subset of the ordinal. Exercise 8 of [TakeutiZaring] p. 42 and its converse.
|- ((A e. C /\ Ord B) -> (A e. B <-> suc A C_ B))