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	endom 7001	Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.)
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵)
Theorem	enrefg 7002	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴)
Theorem	enref 7003	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ≈ 𝐴
Theorem	eqeng 7004	Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵))
Theorem	domrefg 7005	Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≼ 𝐴)
Theorem	en2d 7006*	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.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝑋))    &   ⊢ (𝜑 → (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝑌))    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷)))    ⇒   ⊢ (𝜑 → 𝐴 ≈ 𝐵)
Theorem	en3d 7007*	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.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵))    &   ⊢ (𝜑 → (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴))    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)))    ⇒   ⊢ (𝜑 → 𝐴 ≈ 𝐵)
Theorem	en2i 7008*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 4-Jan-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ V)    &   ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ V)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))    ⇒   ⊢ 𝐴 ≈ 𝐵
Theorem	en3i 7009*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 19-Jul-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)    &   ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶))    ⇒   ⊢ 𝐴 ≈ 𝐵
Theorem	dom2lem 7010*	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.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵))    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴–1-1→𝐵)
Theorem	dom2d 7011*	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.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵))    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦)))    ⇒   ⊢ (𝜑 → (𝐵 ∈ 𝑅 → 𝐴 ≼ 𝐵))
Theorem	dom3d 7012*	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.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵))    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐴 ≼ 𝐵)
Theorem	dom2 7013*	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. 𝐶 and 𝐷 can be read 𝐶(𝑥) and 𝐷(𝑦), as can be inferred from their distinct variable conditions. (Contributed by NM, 26-Oct-2003.)
⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦))    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐴 ≼ 𝐵)
Theorem	dom3 7014*	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. 𝐶 and 𝐷 can be read 𝐶(𝑥) and 𝐷(𝑦), as can be inferred from their distinct variable conditions. (Contributed by Mario Carneiro, 20-May-2013.)
⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ≼ 𝐵)
Theorem	idssen 7015	Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ I ⊆ ≈
Theorem	domssr 7016	If 𝐶 is a superset of 𝐵 and 𝐵 dominates 𝐴, then 𝐶 also dominates 𝐴. (Contributed by BTernaryTau, 7-Dec-2024.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐴 ≼ 𝐵) → 𝐴 ≼ 𝐶)
Theorem	ssdomg 7017	A set dominates its subsets. Theorem 16 of [Suppes] p. 94. (Contributed by NM, 19-Jun-1998.) (Revised by Mario Carneiro, 24-Jun-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))
Theorem	ener 7018	Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ ≈ Er V
Theorem	ensymb 7019	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴)
Theorem	ensym 7020	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
Theorem	ensymi 7021	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    ⇒   ⊢ 𝐵 ≈ 𝐴
Theorem	ensymd 7022	Symmetry of equinumerosity. Deduction form of ensym 7020. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≈ 𝐴)
Theorem	entr 7023	Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)
Theorem	domtr 7024	Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94. (Contributed by NM, 4-Jun-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	entri 7025	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐵 ≈ 𝐶    ⇒   ⊢ 𝐴 ≈ 𝐶
Theorem	entr2i 7026	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐵 ≈ 𝐶    ⇒   ⊢ 𝐶 ≈ 𝐴
Theorem	entr3i 7027	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐴 ≈ 𝐶    ⇒   ⊢ 𝐵 ≈ 𝐶
Theorem	entr4i 7028	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐶 ≈ 𝐵    ⇒   ⊢ 𝐴 ≈ 𝐶
Theorem	endomtr 7029	Transitivity of equinumerosity and dominance. (Contributed by NM, 7-Jun-1998.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	domentr 7030	Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.)
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	f1imaeng 7031	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.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐹 “ 𝐶) ≈ 𝐶)
Theorem	f1imaen2g 7032	A one-to-one function's image under a subset of its domain is equinumerous to the subset. (This version of f1imaen 7033 does not need ax-setind 4658.) (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉)) → (𝐹 “ 𝐶) ≈ 𝐶)
Theorem	f1imaen 7033	A one-to-one function's image under a subset of its domain is equinumerous to the subset. (Contributed by NM, 30-Sep-2004.)
⊢ 𝐶 ∈ V    ⇒   ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 “ 𝐶) ≈ 𝐶)
Theorem	en0 7034	The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.)
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)
Theorem	ensn1 7035	A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ≈ 1o
Theorem	ensn1g 7036	A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ 1o)
Theorem	enpr1g 7037	{𝐴, 𝐴} has only one element. (Contributed by FL, 15-Feb-2010.)
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐴} ≈ 1o)
Theorem	en1 7038*	A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004.)
⊢ (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	en1bg 7039	A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Jim Kingdon, 13-Apr-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ≈ 1o ↔ 𝐴 = {∪ 𝐴}))
Theorem	reuen1 7040*	Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} ≈ 1o)
Theorem	euen1 7041	Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∃!𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≈ 1o)
Theorem	euen1b 7042*	Two ways to express "𝐴 has a unique element". (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ (𝐴 ≈ 1o ↔ ∃!𝑥 𝑥 ∈ 𝐴)
Theorem	en1uniel 7043	A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ (𝑆 ≈ 1o → ∪ 𝑆 ∈ 𝑆)
Theorem	en1m 7044*	A set with one element is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
⊢ (𝐴 ≈ 1o → ∃𝑥 𝑥 ∈ 𝐴)
Theorem	2dom 7045*	A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004.)
⊢ (2o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)
Theorem	fundmen 7046	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.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (Fun 𝐹 → dom 𝐹 ≈ 𝐹)
Theorem	fundmeng 7047	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 17-Sep-2013.)
⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → dom 𝐹 ≈ 𝐹)
Theorem	cnven 7048	A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ ((Rel 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ ◡𝐴)
Theorem	cnvct 7049	If a set is dominated by ω, so is its converse. (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ (𝐴 ≼ ω → ◡𝐴 ≼ ω)
Theorem	fndmeng 7050	A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐴 ≈ 𝐹)
Theorem	mapsnend 7051	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.) (Revised by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 ↑𝑚 {𝐵}) ≈ 𝐴)
Theorem	mapsnen 7052	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.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ↑𝑚 {𝐵}) ≈ 𝐴
Theorem	map1 7053	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.)
⊢ (𝐴 ∈ 𝑉 → (1o ↑𝑚 𝐴) ≈ 1o)
Theorem	en2sn 7054	Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵})
Theorem	snfig 7055	A singleton is finite. For the proper class case, see snprc 3753. (Contributed by Jim Kingdon, 13-Apr-2020.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Fin)
Theorem	fiprc 7056	The class of finite sets is a proper class. (Contributed by Jeff Hankins, 3-Oct-2008.)
⊢ Fin ∉ V
Theorem	unen 7057	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.)
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝐴 ∪ 𝐶) ≈ (𝐵 ∪ 𝐷))
Theorem	en2prd 7058	Two proper unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐷)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ≈ {𝐶, 𝐷})
Theorem	1dom1el 7059	If a set is dominated by one, then any two of its elements are equal. (Contributed by Jim Kingdon, 23-Apr-2025.)
⊢ ((𝐴 ≼ 1o ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → 𝐵 = 𝐶)
Theorem	modom 7060	Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∃*𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≼ 1o)
Theorem	modom2 7061*	Two ways to express "at most one". (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 ≼ 1o)
Theorem	rex2dom 7062*	A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦) → 2o ≼ 𝐴)
Theorem	enpr2d 7063	A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o)
Theorem	en2 7064*	A set equinumerous to ordinal 2 is an unordered pair. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (𝐴 ≈ 2o → ∃𝑥∃𝑦 𝐴 = {𝑥, 𝑦})
Theorem	en2m 7065*	A set with two elements is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
⊢ (𝐴 ≈ 2o → ∃𝑥 𝑥 ∈ 𝐴)
Theorem	ssct 7066	A subset of a set dominated by ω is dominated by ω. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω) → 𝐴 ≼ ω)
Theorem	1domsn 7067	A singleton (whether of a set or a proper class) is dominated by one. (Contributed by Jim Kingdon, 1-Mar-2022.)
⊢ {𝐴} ≼ 1o
Theorem	dom1o 7068*	Two ways of saying that a set is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
⊢ (𝐴 ∈ 𝑉 → (1o ≼ 𝐴 ↔ ∃𝑗 𝑗 ∈ 𝐴))
Theorem	dom1oi 7069	A set with an element dominates one. (Contributed by Jim Kingdon, 3-Feb-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → 1o ≼ 𝐴)
Theorem	enm 7070*	A set equinumerous to an inhabited set is inhabited. (Contributed by Jim Kingdon, 19-May-2020.)
⊢ ((𝐴 ≈ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ 𝐵)
Theorem	xpsnen 7071	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.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 × {𝐵}) ≈ 𝐴
Theorem	xpsneng 7072	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.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × {𝐵}) ≈ 𝐴)
Theorem	xp1en 7073	One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 1o) ≈ 𝐴)
Theorem	endisj 7074*	Any two sets are equinumerous to disjoint sets. Exercise 4.39 of [Mendelson] p. 255. (Contributed by NM, 16-Apr-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∃𝑥∃𝑦((𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵) ∧ (𝑥 ∩ 𝑦) = ∅)
Theorem	xpcomf1o 7075*	The canonical bijection from (𝐴 × 𝐵) to (𝐵 × 𝐴). (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥})    ⇒   ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴)
Theorem	xpcomco 7076*	Composition with the bijection of xpcomf1o 7075 swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥})    &   ⊢ 𝐺 = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶)    ⇒   ⊢ (𝐺 ∘ 𝐹) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	xpcomen 7077	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.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)
Theorem	xpcomeng 7078	Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 27-Mar-2006.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴))
Theorem	xpsnen2g 7079	A set is equinumerous to its Cartesian product with a singleton on the left. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × 𝐵) ≈ 𝐵)
Theorem	xpassen 7080	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.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ ((𝐴 × 𝐵) × 𝐶) ≈ (𝐴 × (𝐵 × 𝐶))
Theorem	xpdom2 7081	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.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ≼ 𝐵 → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
Theorem	xpdom2g 7082	Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
Theorem	xpdom1g 7083	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.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵) → (𝐴 × 𝐶) ≼ (𝐵 × 𝐶))
Theorem	xpdom3m 7084*	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.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ∃𝑥 𝑥 ∈ 𝐵) → 𝐴 ≼ (𝐴 × 𝐵))
Theorem	xpdom1 7085	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.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ≼ 𝐵 → (𝐴 × 𝐶) ≼ (𝐵 × 𝐶))
Theorem	pw2f1odclem 7086*	Lemma for pw2f1odc 7087. (Contributed by Mario Carneiro, 6-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝒫 𝐴DECID 𝑝 ∈ 𝑞)    ⇒   ⊢ (𝜑 → ((𝑆 ∈ 𝒫 𝐴 ∧ 𝐺 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑆, 𝐶, 𝐵))) ↔ (𝐺 ∈ ({𝐵, 𝐶} ↑𝑚 𝐴) ∧ 𝑆 = (◡𝐺 “ {𝐶}))))
Theorem	pw2f1odc 7087*	The power set of a set is equinumerous to set exponentiation with an unordered pair base of ordinal 2. Generalized from Proposition 10.44 of [TakeutiZaring] p. 96. (Contributed by Mario Carneiro, 6-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝒫 𝐴DECID 𝑝 ∈ 𝑞)    &   ⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑥, 𝐶, 𝐵)))    ⇒   ⊢ (𝜑 → 𝐹:𝒫 𝐴–1-1-onto→({𝐵, 𝐶} ↑𝑚 𝐴))
Theorem	fopwdom 7088	Covering implies injection on power sets. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐹 ∈ V ∧ 𝐹:𝐴–onto→𝐵) → 𝒫 𝐵 ≼ 𝒫 𝐴)
Theorem	0domg 7089	Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴)
Theorem	dom0 7090	A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004.)
⊢ (𝐴 ≼ ∅ ↔ 𝐴 = ∅)
Theorem	0dom 7091	Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∅ ≼ 𝐴
Theorem	enen1 7092	Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≈ 𝐶 ↔ 𝐵 ≈ 𝐶))
Theorem	enen2 7093	Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≈ 𝐴 ↔ 𝐶 ≈ 𝐵))
Theorem	domen1 7094	Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≼ 𝐶 ↔ 𝐵 ≼ 𝐶))
Theorem	domen2 7095	Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≼ 𝐴 ↔ 𝐶 ≼ 𝐵))
2.6.30  Equinumerosity (cont.)
Theorem	xpf1o 7096*	Construct a bijection on a Cartesian product given bijections on the factors. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑋):𝐴–1-1-onto→𝐵)    &   ⊢ (𝜑 → (𝑦 ∈ 𝐶 ↦ 𝑌):𝐶–1-1-onto→𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ ⟨𝑋, 𝑌⟩):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷))
Theorem	xpen 7097	Equinumerosity law for Cartesian product. Proposition 4.22(b) of [Mendelson] p. 254. (Contributed by NM, 24-Jul-2004.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 × 𝐶) ≈ (𝐵 × 𝐷))
Theorem	mapen 7098	Two set exponentiations are equinumerous when their bases and exponents are equinumerous. Theorem 6H(c) of [Enderton] p. 139. (Contributed by NM, 16-Dec-2003.) (Proof shortened by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ↑𝑚 𝐶) ≈ (𝐵 ↑𝑚 𝐷))
Theorem	mapdom1g 7099	Order-preserving property of set exponentiation. (Contributed by Jim Kingdon, 15-Jul-2022.)
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝐴 ↑𝑚 𝐶) ≼ (𝐵 ↑𝑚 𝐶))
Theorem	mapxpen 7100	Equinumerosity law for double set exponentiation. Proposition 10.45 of [TakeutiZaring] p. 96. (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ↑𝑚 𝐵) ↑𝑚 𝐶) ≈ (𝐴 ↑𝑚 (𝐵 × 𝐶)))