P. 71 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7001-7100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ixpeq2dva 7001*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
|- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> X_ x e. A B = X_ x e. A C )
Theorem	ixpeq2dv 7002*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
|- ( ph -> B = C )   =>    |- ( ph -> X_ x e. A B = X_ x e. A C )
Theorem	cbvixp 7003*	Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 20-Jun-2011.)
|- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- X_ x e. A B = X_ y e. A C
Theorem	cbvixpv 7004*	Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( x = y -> B = C )   =>    |- X_ x e. A B = X_ y e. A C
Theorem	nfixpxy 7005*	Bound-variable hypothesis builder for indexed Cartesian product. (Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by Jim Kingdon, 15-Feb-2023.)
|- F/_ y A   &    |- F/_ y B   =>    |- F/_ y X_ x e. A B
Theorem	nfixp1 7006	The index variable in an indexed Cartesian product is not free. (Contributed by Jeff Madsen, 19-Jun-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x X_ x e. A B
Theorem	ixpprc 7007*	A cartesian product of proper-class many sets is empty, because any function in the cartesian product has to be a set with domain A, which is not possible for a proper class domain. (Contributed by Mario Carneiro, 25-Jan-2015.)
|- ( -. A e. _V -> X_ x e. A B = (/) )
Theorem	ixpf 7008*	A member of an infinite Cartesian product maps to the indexed union of the product argument. Remark in [Enderton] p. 54. (Contributed by NM, 28-Sep-2006.)
|- ( F e. X_ x e. A B -> F : A --> U_ x e. A B )
Theorem	uniixp 7009*	The union of an infinite Cartesian product is included in a Cartesian product. (Contributed by NM, 28-Sep-2006.) (Revised by Mario Carneiro, 24-Jun-2015.)
|- U. X_ x e. A B C_ ( A X. U_ x e. A B )
Theorem	ixpexgg 7010*	The existence of an infinite Cartesian product. x is normally a free-variable parameter in B. Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006.) (Revised by Jim Kingdon, 15-Feb-2023.)
|- ( ( A e. W /\ A. x e. A B e. V ) -> X_ x e. A B e. _V )
Theorem	ixpin 7011*	The intersection of two infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- X_ x e. A ( B i^i C ) = ( X_ x e. A B i^i X_ x e. A C )
Theorem	ixpiinm 7012*	The indexed intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 6-Feb-2015.) (Revised by Jim Kingdon, 15-Feb-2023.)
|- ( E. z z e. B -> X_ x e. A |^|_ y e. B C = |^|_ y e. B X_ x e. A C )
Theorem	ixpintm 7013*	The intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Jim Kingdon, 15-Feb-2023.)
|- ( E. z z e. B -> X_ x e. A |^| B = |^|_ y e. B X_ x e. A y )
Theorem	ixp0x 7014	An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007.)
|- X_ x e. (/) A = { (/) }
Theorem	ixpssmap2g 7015*	An infinite Cartesian product is a subset of set exponentiation. This version of ixpssmapg 7016 avoids ax-coll 4248. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( U_ x e. A B e. V -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
Theorem	ixpssmapg 7016*	An infinite Cartesian product is a subset of set exponentiation. (Contributed by Jeff Madsen, 19-Jun-2011.)
|- ( A. x e. A B e. V -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
Theorem	0elixp 7017	Membership of the empty set in an infinite Cartesian product. (Contributed by Steve Rodriguez, 29-Sep-2006.)
|- (/) e. X_ x e. (/) A
Theorem	ixpm 7018*	If an infinite Cartesian product of a family B ( x ) is inhabited, every B ( x ) is inhabited. (Contributed by Mario Carneiro, 22-Jun-2016.) (Revised by Jim Kingdon, 16-Feb-2023.)
|- ( E. f f e. X_ x e. A B -> A. x e. A E. z z e. B )
Theorem	ixp0 7019	The infinite Cartesian product of a family B ( x ) with an empty member is empty. (Contributed by NM, 1-Oct-2006.) (Revised by Jim Kingdon, 16-Feb-2023.)
|- ( E. x e. A B = (/) -> X_ x e. A B = (/) )
Theorem	ixpssmap 7020*	An infinite Cartesian product is a subset of set exponentiation. Remark in [Enderton] p. 54. (Contributed by NM, 28-Sep-2006.)
|- B e. _V   =>    |- X_ x e. A B C_ ( U_ x e. A B ^m A )
Theorem	resixp 7021*	Restriction of an element of an infinite Cartesian product. (Contributed by FL, 7-Nov-2011.) (Proof shortened by Mario Carneiro, 31-May-2014.)
|- ( ( B C_ A /\ F e. X_ x e. A C ) -> ( F |` B ) e. X_ x e. B C )
Theorem	mptelixpg 7022*	Condition for an explicit member of an indexed product. (Contributed by Stefan O'Rear, 4-Jan-2015.)
|- ( I e. V -> ( ( x e. I |-> J ) e. X_ x e. I K <-> A. x e. I J e. K ) )
Theorem	elixpsn 7023*	Membership in a class of singleton functions. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( A e. V -> ( F e. X_ x e. { A } B <-> E. y e. B F = { <. A , y >. } ) )
Theorem	ixpsnf1o 7024*	A bijection between a class and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- F = ( x e. A |-> ( { I } X. { x } ) )   =>    |- ( I e. V -> F : A -1-1-onto-> X_ y e. { I } A )
Theorem	mapsnf1o 7025*	A bijection between a set and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- F = ( x e. A |-> ( { I } X. { x } ) )   =>    |- ( ( A e. V /\ I e. W ) -> F : A -1-1-onto-> ( A ^m { I } ) )
2.6.29  Equinumerosity
Syntax	cen 7026	Extend class definition to include the equinumerosity relation ("approximately equals" symbol)
class ~~
Syntax	cdom 7027	Extend class definition to include the dominance relation (curly less-than-or-equal)
class ~<_
Syntax	cfn 7028	Extend class definition to include the class of all finite sets.
class Fin
Definition	df-en 7029*	Define the equinumerosity relation. Definition of [Enderton] p. 129. We define ~~ to be a binary relation rather than a connective, so its arguments must be sets to be meaningful. This is acceptable because we do not consider equinumerosity for proper classes. We derive the usual definition as bren 7036. (Contributed by NM, 28-Mar-1998.)
|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
Definition	df-dom 7030*	Define the dominance relation. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 7040 and domen 7041. (Contributed by NM, 28-Mar-1998.)
|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
Definition	df-fin 7031*	Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our " a e. Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 17224. (Contributed by NM, 22-Aug-2008.)
|- Fin = { x | E. y e. om x ~~ y }
Theorem	relen 7032	Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
|- Rel ~~
Theorem	reldom 7033	Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
|- Rel ~<_
Theorem	encv 7034	If two classes are equinumerous, both classes are sets. (Contributed by AV, 21-Mar-2019.)
|- ( A ~~ B -> ( A e. _V /\ B e. _V ) )
Theorem	breng 7035*	Equinumerosity relation. This variation of bren 7036 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of bren 7036. (Revised by BTernaryTau, 23-Sep-2024.)
|- ( ( A e. V /\ B e. W ) -> ( A ~~ B <-> E. f f : A -1-1-onto-> B ) )
Theorem	bren 7036*	Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
|- ( A ~~ B <-> E. f f : A -1-1-onto-> B )
Theorem	brdom2g 7037*	Dominance relation. This variation of brdomg 7038 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of brdomg 7038. (Revised by BTernaryTau, 29-Nov-2024.)
|- ( ( A e. V /\ B e. W ) -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
Theorem	brdomg 7038*	Dominance relation. (Contributed by NM, 15-Jun-1998.)
|- ( B e. C -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
Theorem	brdomi 7039*	Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( A ~<_ B -> E. f f : A -1-1-> B )
Theorem	brdom 7040*	Dominance relation. (Contributed by NM, 15-Jun-1998.)
|- B e. _V   =>    |- ( A ~<_ B <-> E. f f : A -1-1-> B )
Theorem	domen 7041*	Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146. (Contributed by NM, 15-Jun-1998.)
|- B e. _V   =>    |- ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) )
Theorem	domeng 7042*	Dominance in terms of equinumerosity, with the sethood requirement expressed as an antecedent. Example 1 of [Enderton] p. 146. (Contributed by NM, 24-Apr-2004.)
|- ( B e. C -> ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) ) )
Theorem	ctex 7043	A class dominated by om is a set. See also ctfoex 7464 which says that a countable class is a set. (Contributed by Thierry Arnoux, 29-Dec-2016.) (Proof shortened by Jim Kingdon, 13-Mar-2023.)
|- ( A ~<_ om -> A e. _V )
Theorem	f1oen4g 7044	The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng 7049 does not require the Axiom of Collection nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.)
|- ( ( ( F e. V /\ A e. W /\ B e. X ) /\ F : A -1-1-onto-> B ) -> A ~~ B )
Theorem	f1dom4g 7045	The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg 7050 does not require the Axiom of Collection nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.)
|- ( ( ( F e. V /\ A e. W /\ B e. X ) /\ F : A -1-1-> B ) -> A ~<_ B )
Theorem	f1oen3g 7046	The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 7049 does not require the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro, 10-Sep-2015.)
|- ( ( F e. V /\ F : A -1-1-onto-> B ) -> A ~~ B )
Theorem	f1oen2g 7047	The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 7049 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( ( A e. V /\ B e. W /\ F : A -1-1-onto-> B ) -> A ~~ B )
Theorem	f1dom2g 7048	The domain of a one-to-one function is dominated by its codomain. This variation of f1domg 7050 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( ( A e. V /\ B e. W /\ F : A -1-1-> B ) -> A ~<_ B )
Theorem	f1oeng 7049	The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)
|- ( ( A e. C /\ F : A -1-1-onto-> B ) -> A ~~ B )
Theorem	f1domg 7050	The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004.)
|- ( B e. C -> ( F : A -1-1-> B -> A ~<_ B ) )
Theorem	f1oen 7051	The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)
|- A e. _V   =>    |- ( F : A -1-1-onto-> B -> A ~~ B )
Theorem	f1dom 7052	The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 19-Jun-1998.)
|- B e. _V   =>    |- ( F : A -1-1-> B -> A ~<_ B )
Theorem	isfi 7053*	Express " A is finite". Definition 10.29 of [TakeutiZaring] p. 91 (whose " Fin " is a predicate instead of a class). (Contributed by NM, 22-Aug-2008.)
|- ( A e. Fin <-> E. x e. om A ~~ x )
Theorem	enssdom 7054	Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
|- ~~ C_ ~<_
Theorem	endom 7055	Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.)
|- ( A ~~ B -> A ~<_ B )
Theorem	enrefg 7056	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A e. V -> A ~~ A )
Theorem	enref 7057	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
|- A e. _V   =>    |- A ~~ A
Theorem	eqeng 7058	Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
|- ( A e. V -> ( A = B -> A ~~ B ) )
Theorem	domrefg 7059	Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
|- ( A e. V -> A ~<_ A )
Theorem	en2d 7060*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by AV, 4-Aug-2024.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> ( x e. A -> C e. X ) )   &    |- ( ph -> ( y e. B -> D e. Y ) )   &    |- ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) )   =>    |- ( ph -> A ~~ B )
Theorem	en3d 7061*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by AV, 4-Aug-2024.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> ( x e. A -> C e. B ) )   &    |- ( ph -> ( y e. B -> D e. A ) )   &    |- ( ph -> ( ( x e. A /\ y e. B ) -> ( x = D <-> y = C ) ) )   =>    |- ( ph -> A ~~ B )
Theorem	en2i 7062*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 4-Jan-2004.)
|- A e. _V   &    |- B e. _V   &    |- ( x e. A -> C e. _V )   &    |- ( y e. B -> D e. _V )   &    |- ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) )   =>    |- A ~~ B
Theorem	en3i 7063*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 19-Jul-2004.)
|- A e. _V   &    |- B e. _V   &    |- ( x e. A -> C e. B )   &    |- ( y e. B -> D e. A )   &    |- ( ( x e. A /\ y e. B ) -> ( x = D <-> y = C ) )   =>    |- A ~~ B
Theorem	dom2lem 7064*	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004.)
|- ( ph -> ( x e. A -> C e. B ) )   &    |- ( ph -> ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) ) )   =>    |- ( ph -> ( x e. A |-> C ) : A -1-1-> B )
Theorem	dom2d 7065*	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 20-May-2013.)
|- ( ph -> ( x e. A -> C e. B ) )   &    |- ( ph -> ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) ) )   =>    |- ( ph -> ( B e. R -> A ~<_ B ) )
Theorem	dom3d 7066*	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by Mario Carneiro, 20-May-2013.)
|- ( ph -> ( x e. A -> C e. B ) )   &    |- ( ph -> ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> A ~<_ B )
Theorem	dom2 7067*	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. C and D can be read C ( x ) and D ( y ), as can be inferred from their distinct variable conditions. (Contributed by NM, 26-Oct-2003.)
|- ( x e. A -> C e. B )   &    |- ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) )   =>    |- ( B e. V -> A ~<_ B )
Theorem	dom3 7068*	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. C and D can be read C ( x ) and D ( y ), as can be inferred from their distinct variable conditions. (Contributed by Mario Carneiro, 20-May-2013.)
|- ( x e. A -> C e. B )   &    |- ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) )   =>    |- ( ( A e. V /\ B e. W ) -> A ~<_ B )
Theorem	idssen 7069	Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- _I C_ ~~
Theorem	domssr 7070	If C is a superset of B and B dominates A, then C also dominates A. (Contributed by BTernaryTau, 7-Dec-2024.)
|- ( ( C e. V /\ B C_ C /\ A ~<_ B ) -> A ~<_ C )
Theorem	ssdomg 7071	A set dominates its subsets. Theorem 16 of [Suppes] p. 94. (Contributed by NM, 19-Jun-1998.) (Revised by Mario Carneiro, 24-Jun-2015.)
|- ( B e. V -> ( A C_ B -> A ~<_ B ) )
Theorem	ener 7072	Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ~~ Er _V
Theorem	ensymb 7073	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( A ~~ B <-> B ~~ A )
Theorem	ensym 7074	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A ~~ B -> B ~~ A )
Theorem	ensymi 7075	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   =>    |- B ~~ A
Theorem	ensymd 7076	Symmetry of equinumerosity. Deduction form of ensym 7074. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A ~~ B )   =>    |- ( ph -> B ~~ A )
Theorem	entr 7077	Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.)
|- ( ( A ~~ B /\ B ~~ C ) -> A ~~ C )
Theorem	domtr 7078	Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94. (Contributed by NM, 4-Jun-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A ~<_ B /\ B ~<_ C ) -> A ~<_ C )
Theorem	entri 7079	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   &    |- B ~~ C   =>    |- A ~~ C
Theorem	entr2i 7080	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   &    |- B ~~ C   =>    |- C ~~ A
Theorem	entr3i 7081	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   &    |- A ~~ C   =>    |- B ~~ C
Theorem	entr4i 7082	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   &    |- C ~~ B   =>    |- A ~~ C
Theorem	endomtr 7083	Transitivity of equinumerosity and dominance. (Contributed by NM, 7-Jun-1998.)
|- ( ( A ~~ B /\ B ~<_ C ) -> A ~<_ C )
Theorem	domentr 7084	Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.)
|- ( ( A ~<_ B /\ B ~~ C ) -> A ~<_ C )
Theorem	f1imaeng 7085	A one-to-one function's image under a subset of its domain is equinumerous to the subset. (Contributed by Mario Carneiro, 15-May-2015.)
|- ( ( F : A -1-1-> B /\ C C_ A /\ C e. V ) -> ( F " C ) ~~ C )
Theorem	f1imaen2g 7086	A one-to-one function's image under a subset of its domain is equinumerous to the subset. (This version of f1imaen 7087 does not need ax-setind 4686.) (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.)
|- ( ( ( F : A -1-1-> B /\ B e. V ) /\ ( C C_ A /\ C e. V ) ) -> ( F " C ) ~~ C )
Theorem	f1imaen 7087	A one-to-one function's image under a subset of its domain is equinumerous to the subset. (Contributed by NM, 30-Sep-2004.)
|- C e. _V   =>    |- ( ( F : A -1-1-> B /\ C C_ A ) -> ( F " C ) ~~ C )
Theorem	en0 7088	The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.)
|- ( A ~~ (/) <-> A = (/) )
Theorem	ensn1 7089	A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.)
|- A e. _V   =>    |- { A } ~~ 1o
Theorem	ensn1g 7090	A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004.)
|- ( A e. V -> { A } ~~ 1o )
Theorem	enpr1g 7091	{ A , A } has only one element. (Contributed by FL, 15-Feb-2010.)
|- ( A e. V -> { A , A } ~~ 1o )
Theorem	en1 7092*	A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004.)
|- ( A ~~ 1o <-> E. x A = { x } )
Theorem	en1bg 7093	A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Jim Kingdon, 13-Apr-2020.)
|- ( A e. V -> ( A ~~ 1o <-> A = { U. A } ) )
Theorem	reuen1 7094*	Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
|- ( E! x e. A ph <-> { x e. A | ph } ~~ 1o )
Theorem	euen1 7095	Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
|- ( E! x ph <-> { x | ph } ~~ 1o )
Theorem	euen1b 7096*	Two ways to express " A has a unique element". (Contributed by Mario Carneiro, 9-Apr-2015.)
|- ( A ~~ 1o <-> E! x x e. A )
Theorem	en1uniel 7097	A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015.)
|- ( S ~~ 1o -> U. S e. S )
Theorem	en1m 7098*	A set with one element is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
|- ( A ~~ 1o -> E. x x e. A )
Theorem	2dom 7099*	A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004.)
|- ( 2o ~<_ A -> E. x e. A E. y e. A -. x = y )
Theorem	fundmen 7100	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 28-Jul-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- F e. _V   =>    |- ( Fun F -> dom F ~~ F )