P. 68 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6701-6800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	relen 6701	Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
|- Rel ~~
Theorem	reldom 6702	Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
|- Rel ~<_
Theorem	encv 6703	If two classes are equinumerous, both classes are sets. (Contributed by AV, 21-Mar-2019.)
|- ( A ~~ B -> ( A e. _V /\ B e. _V ) )
Theorem	bren 6704*	Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
|- ( A ~~ B <-> E. f f : A -1-1-onto-> B )
Theorem	brdomg 6705*	Dominance relation. (Contributed by NM, 15-Jun-1998.)
|- ( B e. C -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
Theorem	brdomi 6706*	Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( A ~<_ B -> E. f f : A -1-1-> B )
Theorem	brdom 6707*	Dominance relation. (Contributed by NM, 15-Jun-1998.)
|- B e. _V   =>    |- ( A ~<_ B <-> E. f f : A -1-1-> B )
Theorem	domen 6708*	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 6709*	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 6710	A class dominated by om is a set. See also ctfoex 7074 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	f1oen3g 6711	The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 6714 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 6712	The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 6714 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 6713	The domain of a one-to-one function is dominated by its codomain. This variation of f1domg 6715 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 6714	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 6715	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 6716	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 6717	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 6718*	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 6719	Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
|- ~~ C_ ~<_
Theorem	endom 6720	Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.)
|- ( A ~~ B -> A ~<_ B )
Theorem	enrefg 6721	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 6722	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
|- A e. _V   =>    |- A ~~ A
Theorem	eqeng 6723	Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
|- ( A e. V -> ( A = B -> A ~~ B ) )
Theorem	domrefg 6724	Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
|- ( A e. V -> A ~<_ A )
Theorem	en2d 6725*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.)
|- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> ( x e. A -> C e. _V ) )   &    |- ( ph -> ( y e. B -> D e. _V ) )   &    |- ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) )   =>    |- ( ph -> A ~~ B )
Theorem	en3d 6726*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.)
|- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( 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 6727*	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 6728*	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 6729*	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 6730*	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 6731*	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 6732*	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 6733*	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 6734	Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- _I C_ ~~
Theorem	ssdomg 6735	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 6736	Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ~~ Er _V
Theorem	ensymb 6737	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( A ~~ B <-> B ~~ A )
Theorem	ensym 6738	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 6739	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   =>    |- B ~~ A
Theorem	ensymd 6740	Symmetry of equinumerosity. Deduction form of ensym 6738. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A ~~ B )   =>    |- ( ph -> B ~~ A )
Theorem	entr 6741	Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.)
|- ( ( A ~~ B /\ B ~~ C ) -> A ~~ C )
Theorem	domtr 6742	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 6743	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   &    |- B ~~ C   =>    |- A ~~ C
Theorem	entr2i 6744	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   &    |- B ~~ C   =>    |- C ~~ A
Theorem	entr3i 6745	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   &    |- A ~~ C   =>    |- B ~~ C
Theorem	entr4i 6746	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   &    |- C ~~ B   =>    |- A ~~ C
Theorem	endomtr 6747	Transitivity of equinumerosity and dominance. (Contributed by NM, 7-Jun-1998.)
|- ( ( A ~~ B /\ B ~<_ C ) -> A ~<_ C )
Theorem	domentr 6748	Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.)
|- ( ( A ~<_ B /\ B ~~ C ) -> A ~<_ C )
Theorem	f1imaeng 6749	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 6750	A one-to-one function's image under a subset of its domain is equinumerous to the subset. (This version of f1imaen 6751 does not need ax-setind 4508.) (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 6751	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 6752	The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.)
|- ( A ~~ (/) <-> A = (/) )
Theorem	ensn1 6753	A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.)
|- A e. _V   =>    |- { A } ~~ 1o
Theorem	ensn1g 6754	A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004.)
|- ( A e. V -> { A } ~~ 1o )
Theorem	enpr1g 6755	{ A , A } has only one element. (Contributed by FL, 15-Feb-2010.)
|- ( A e. V -> { A , A } ~~ 1o )
Theorem	en1 6756*	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 6757	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 6758*	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 6759	Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
|- ( E! x ph <-> { x | ph } ~~ 1o )
Theorem	euen1b 6760*	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 6761	A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015.)
|- ( S ~~ 1o -> U. S e. S )
Theorem	2dom 6762*	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 6763	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 )
Theorem	fundmeng 6764	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 17-Sep-2013.)
|- ( ( F e. V /\ Fun F ) -> dom F ~~ F )
Theorem	cnven 6765	A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- ( ( Rel A /\ A e. V ) -> A ~~ `' A )
Theorem	cnvct 6766	If a set is dominated by om, so is its converse. (Contributed by Thierry Arnoux, 29-Dec-2016.)
|- ( A ~<_ om -> `' A ~<_ om )
Theorem	fndmeng 6767	A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ( F Fn A /\ A e. C ) -> A ~~ F )
Theorem	mapsnen 6768	Set exponentiation to a singleton exponent is equinumerous to its base. Exercise 4.43 of [Mendelson] p. 255. (Contributed by NM, 17-Dec-2003.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- A e. _V   &    |- B e. _V   =>    |- ( A ^m { B } ) ~~ A
Theorem	map1 6769	Set exponentiation: ordinal 1 to any set is equinumerous to ordinal 1. Exercise 4.42(b) of [Mendelson] p. 255. (Contributed by NM, 17-Dec-2003.)
|- ( A e. V -> ( 1o ^m A ) ~~ 1o )
Theorem	en2sn 6770	Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.)
|- ( ( A e. C /\ B e. D ) -> { A } ~~ { B } )
Theorem	snfig 6771	A singleton is finite. For the proper class case, see snprc 3635. (Contributed by Jim Kingdon, 13-Apr-2020.)
|- ( A e. V -> { A } e. Fin )
Theorem	fiprc 6772	The class of finite sets is a proper class. (Contributed by Jeff Hankins, 3-Oct-2008.)
|- Fin e/ _V
Theorem	unen 6773	Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( ( ( A ~~ B /\ C ~~ D ) /\ ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( A u. C ) ~~ ( B u. D ) )
Theorem	enpr2d 6774	A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- ( ph -> A e. C )   &    |- ( ph -> B e. D )   &    |- ( ph -> -. A = B )   =>    |- ( ph -> { A , B } ~~ 2o )
Theorem	ssct 6775	A subset of a set dominated by om is dominated by om. (Contributed by Thierry Arnoux, 31-Jan-2017.)
|- ( ( A C_ B /\ B ~<_ om ) -> A ~<_ om )
Theorem	1domsn 6776	A singleton (whether of a set or a proper class) is dominated by one. (Contributed by Jim Kingdon, 1-Mar-2022.)
|- { A } ~<_ 1o
Theorem	enm 6777*	A set equinumerous to an inhabited set is inhabited. (Contributed by Jim Kingdon, 19-May-2020.)
|- ( ( A ~~ B /\ E. x x e. A ) -> E. y y e. B )
Theorem	xpsnen 6778	A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254. (Contributed by NM, 4-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- A e. _V   &    |- B e. _V   =>    |- ( A X. { B } ) ~~ A
Theorem	xpsneng 6779	A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254. (Contributed by NM, 22-Oct-2004.)
|- ( ( A e. V /\ B e. W ) -> ( A X. { B } ) ~~ A )
Theorem	xp1en 6780	One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( A e. V -> ( A X. 1o ) ~~ A )
Theorem	endisj 6781*	Any two sets are equinumerous to disjoint sets. Exercise 4.39 of [Mendelson] p. 255. (Contributed by NM, 16-Apr-2004.)
|- A e. _V   &    |- B e. _V   =>    |- E. x E. y ( ( x ~~ A /\ y ~~ B ) /\ ( x i^i y ) = (/) )
Theorem	xpcomf1o 6782*	The canonical bijection from ( A X. B ) to ( B X. A ). (Contributed by Mario Carneiro, 23-Apr-2014.)
|- F = ( x e. ( A X. B ) |-> U. `' { x } )   =>    |- F : ( A X. B ) -1-1-onto-> ( B X. A )
Theorem	xpcomco 6783*	Composition with the bijection of xpcomf1o 6782 swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015.)
|- F = ( x e. ( A X. B ) |-> U. `' { x } )   &    |- G = ( y e. B , z e. A |-> C )   =>    |- ( G o. F ) = ( z e. A , y e. B |-> C )
Theorem	xpcomen 6784	Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 5-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- A e. _V   &    |- B e. _V   =>    |- ( A X. B ) ~~ ( B X. A )
Theorem	xpcomeng 6785	Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 27-Mar-2006.)
|- ( ( A e. V /\ B e. W ) -> ( A X. B ) ~~ ( B X. A ) )
Theorem	xpsnen2g 6786	A set is equinumerous to its Cartesian product with a singleton on the left. (Contributed by Stefan O'Rear, 21-Nov-2014.)
|- ( ( A e. V /\ B e. W ) -> ( { A } X. B ) ~~ B )
Theorem	xpassen 6787	Associative law for equinumerosity of Cartesian product. Proposition 4.22(e) of [Mendelson] p. 254. (Contributed by NM, 22-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( ( A X. B ) X. C ) ~~ ( A X. ( B X. C ) )
Theorem	xpdom2 6788	Dominance law for Cartesian product. Proposition 10.33(2) of [TakeutiZaring] p. 92. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- C e. _V   =>    |- ( A ~<_ B -> ( C X. A ) ~<_ ( C X. B ) )
Theorem	xpdom2g 6789	Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( ( C e. V /\ A ~<_ B ) -> ( C X. A ) ~<_ ( C X. B ) )
Theorem	xpdom1g 6790	Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 25-Mar-2006.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( ( C e. V /\ A ~<_ B ) -> ( A X. C ) ~<_ ( B X. C ) )
Theorem	xpdom3m 6791*	A set is dominated by its Cartesian product with an inhabited set. Exercise 6 of [Suppes] p. 98. (Contributed by Jim Kingdon, 15-Apr-2020.)
|- ( ( A e. V /\ B e. W /\ E. x x e. B ) -> A ~<_ ( A X. B ) )
Theorem	xpdom1 6792	Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 28-Sep-2004.) (Revised by NM, 29-Mar-2006.) (Revised by Mario Carneiro, 7-May-2015.)
|- C e. _V   =>    |- ( A ~<_ B -> ( A X. C ) ~<_ ( B X. C ) )
Theorem	fopwdom 6793	Covering implies injection on power sets. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.)
|- ( ( F e. _V /\ F : A -onto-> B ) -> ~P B ~<_ ~P A )
Theorem	0domg 6794	Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A e. V -> (/) ~<_ A )
Theorem	dom0 6795	A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004.)
|- ( A ~<_ (/) <-> A = (/) )
Theorem	0dom 6796	Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- A e. _V   =>    |- (/) ~<_ A
Theorem	enen1 6797	Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.)
|- ( A ~~ B -> ( A ~~ C <-> B ~~ C ) )
Theorem	enen2 6798	Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.)
|- ( A ~~ B -> ( C ~~ A <-> C ~~ B ) )
Theorem	domen1 6799	Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.)
|- ( A ~~ B -> ( A ~<_ C <-> B ~<_ C ) )
Theorem	domen2 6800	Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.)
|- ( A ~~ B -> ( C ~<_ A <-> C ~<_ B ) )