P. 90 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8901-9000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	reldom 8901	Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
⊢ Rel ≼
Theorem	relsdom 8902	Strict dominance is a relation. (Contributed by NM, 31-Mar-1998.)
⊢ Rel ≺
Theorem	encv 8903	If two classes are equinumerous, both classes are sets. (Contributed by AV, 21-Mar-2019.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	breng 8904*	Equinumerosity relation. This variation of bren 8905 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of bren 8905. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
Theorem	bren 8905*	Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8904 as an intermediate result. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)
Theorem	brdom2g 8906*	Dominance relation. This variation of brdomg 8907 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of brdomg 8907. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
Theorem	brdomg 8907*	Dominance relation. (Contributed by NM, 15-Jun-1998.) Extract brdom2g 8906 as an intermediate result. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
Theorem	brdomi 8908*	Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.) Avoid ax-un 7690. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵)
Theorem	brdom 8909*	Dominance relation. (Contributed by NM, 15-Jun-1998.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)
Theorem	domen 8910*	Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146. (Contributed by NM, 15-Jun-1998.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))
Theorem	domeng 8911*	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.)
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)))
Theorem	ctex 8912	A countable set is a set. (Contributed by Thierry Arnoux, 29-Dec-2016.) (Proof shortened by Jim Kingdon, 13-Mar-2023.)
⊢ (𝐴 ≼ ω → 𝐴 ∈ V)
Theorem	f1oen4g 8913	The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng 8919 does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.)
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1dom4g 8914	The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg 8920 does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.)
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
Theorem	f1oen3g 8915	The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng 8919 does not require the Axiom of Replacement nor the Axiom of Power Sets. (Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1dom3g 8916	The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg 8920 does not require the Axiom of Replacement nor the Axiom of Power Sets. (Contributed by BTernaryTau, 9-Sep-2024.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
Theorem	f1oen2g 8917	The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 8919 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1dom2g 8918	The domain of a one-to-one function is dominated by its codomain. This variation of f1domg 8920 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.) (Proof shortened by BTernaryTau, 25-Sep-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
Theorem	f1oeng 8919	The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1domg 8920	The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004.)
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵))
Theorem	f1oen 8921	The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐴 ≈ 𝐵)
Theorem	f1dom 8922	The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 19-Jun-1998.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵)
Theorem	brsdom 8923	Strict dominance relation, meaning "𝐵 is strictly greater in size than 𝐴". Definition of [Mendelson] p. 255. (Contributed by NM, 25-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵))
Theorem	isfi 8924*	Express "𝐴 is finite". Definition 10.29 of [TakeutiZaring] p. 91 (whose "Fin " is a predicate instead of a class). (Contributed by NM, 22-Aug-2008.)
⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
Theorem	enssdom 8925	Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.) (Proof shortened by TM, 10-Feb-2026.)
⊢ ≈ ⊆ ≼
Theorem	enssdomOLD 8926	Obsolete version of enssdom 8925 as of 10-Feb-2026. (Contributed by NM, 31-Mar-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ≈ ⊆ ≼
Theorem	dfdom2 8927	Alternate definition of dominance. (Contributed by NM, 17-Jun-1998.)
⊢ ≼ = ( ≺ ∪ ≈ )
Theorem	endom 8928	Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.)
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵)
Theorem	sdomdom 8929	Strict dominance implies dominance. (Contributed by NM, 10-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵)
Theorem	sdomnen 8930	Strict dominance implies non-equinumerosity. (Contributed by NM, 10-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵)
Theorem	brdom2 8931	Dominance in terms of strict dominance and equinumerosity. Theorem 22(iv) of [Suppes] p. 97. (Contributed by NM, 17-Jun-1998.)
⊢ (𝐴 ≼ 𝐵 ↔ (𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵))
Theorem	bren2 8932	Equinumerosity expressed in terms of dominance and strict dominance. (Contributed by NM, 23-Oct-2004.)
⊢ (𝐴 ≈ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵))
Theorem	enrefg 8933	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴)
Theorem	enref 8934	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ≈ 𝐴
Theorem	eqeng 8935	Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵))
Theorem	domrefg 8936	Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≼ 𝐴)
Theorem	en2d 8937*	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 8938*	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 8939*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 4-Jan-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ V)    &   ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ V)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))    ⇒   ⊢ 𝐴 ≈ 𝐵
Theorem	en3i 8940*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 19-Jul-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)    &   ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶))    ⇒   ⊢ 𝐴 ≈ 𝐵
Theorem	dom2lem 8941*	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 8942*	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 8943*	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 8944*	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 8945*	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 8946	Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ I ⊆ ≈
Theorem	domssl 8947	If 𝐴 is a subset of 𝐵 and 𝐶 dominates 𝐵, then 𝐶 also dominates 𝐴. (Contributed by BTernaryTau, 7-Dec-2024.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	domssr 8948	If 𝐶 is a superset of 𝐵 and 𝐵 dominates 𝐴, then 𝐶 also dominates 𝐴. (Contributed by BTernaryTau, 7-Dec-2024.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐴 ≼ 𝐵) → 𝐴 ≼ 𝐶)
Theorem	ssdomg 8949	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 8950	Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.) (Proof shortened by AV, 1-May-2021.)
⊢ ≈ Er V
Theorem	ensymb 8951	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴)
Theorem	ensym 8952	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
Theorem	ensymi 8953	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    ⇒   ⊢ 𝐵 ≈ 𝐴
Theorem	ensymd 8954	Symmetry of equinumerosity. Deduction form of ensym 8952. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≈ 𝐴)
Theorem	entr 8955	Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)
Theorem	domtr 8956	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 8957	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐵 ≈ 𝐶    ⇒   ⊢ 𝐴 ≈ 𝐶
Theorem	entr2i 8958	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐵 ≈ 𝐶    ⇒   ⊢ 𝐶 ≈ 𝐴
Theorem	entr3i 8959	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐴 ≈ 𝐶    ⇒   ⊢ 𝐵 ≈ 𝐶
Theorem	entr4i 8960	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐶 ≈ 𝐵    ⇒   ⊢ 𝐴 ≈ 𝐶
Theorem	endomtr 8961	Transitivity of equinumerosity and dominance. (Contributed by NM, 7-Jun-1998.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	domentr 8962	Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.)
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	f1imaeng 8963	If a function is one-to-one, then the image of a subset of its domain under it is equinumerous to the subset. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐹 “ 𝐶) ≈ 𝐶)
Theorem	f1imaen2g 8964	If a function is one-to-one, then the image of a subset of its domain under it is equinumerous to the subset. (This version of f1imaeng 8963 does not need ax-rep 5226.) (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉)) → (𝐹 “ 𝐶) ≈ 𝐶)
Theorem	f1imaen3g 8965	If a set function is one-to-one, then a subset of its domain is equinumerous to the image of that subset. (This version of f1imaeng 8963 does not need ax-rep 5226 nor ax-pow 5312.) (Contributed by BTernaryTau, 13-Jan-2025.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ 𝑉) → 𝐶 ≈ (𝐹 “ 𝐶))
Theorem	f1imaen 8966	If a function is one-to-one, then the image of a subset of its domain under it is equinumerous to the subset. (Contributed by NM, 30-Sep-2004.)
⊢ 𝐶 ∈ V    ⇒   ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 “ 𝐶) ≈ 𝐶)
Theorem	en0 8967	The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.) Avoid ax-pow 5312, ax-un 7690. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)
Theorem	en0ALT 8968	Shorter proof of en0 8967, depending on ax-pow 5312 and ax-un 7690. (Contributed by NM, 27-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)
Theorem	en0r 8969	The empty set is equinumerous only to itself. (Contributed by BTernaryTau, 29-Nov-2024.)
⊢ (∅ ≈ 𝐴 ↔ 𝐴 = ∅)
Theorem	ensn1 8970	A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.) Avoid ax-un 7690. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ≈ 1o
Theorem	ensn1g 8971	A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ 1o)
Theorem	enpr1g 8972	{𝐴, 𝐴} has only one element. (Contributed by FL, 15-Feb-2010.)
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐴} ≈ 1o)
Theorem	en1 8973*	A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004.) Avoid ax-un 7690. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	en1b 8974	A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015.) Avoid ax-un 7690. (Revised by BTernaryTau, 24-Sep-2024.)
⊢ (𝐴 ≈ 1o ↔ 𝐴 = {∪ 𝐴})
Theorem	reuen1 8975*	Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} ≈ 1o)
Theorem	euen1 8976	Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∃!𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≈ 1o)
Theorem	euen1b 8977*	Two ways to express "𝐴 has a unique element". (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ (𝐴 ≈ 1o ↔ ∃!𝑥 𝑥 ∈ 𝐴)
Theorem	en1uniel 8978	A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015.) Avoid ax-un 7690. (Revised by BTernaryTau, 24-Sep-2024.)
⊢ (𝑆 ≈ 1o → ∪ 𝑆 ∈ 𝑆)
Theorem	2dom 8979*	A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004.)
⊢ (2o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)
Theorem	fundmen 8980	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 8981	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 17-Sep-2013.)
⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → dom 𝐹 ≈ 𝐹)
Theorem	cnven 8982	A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ ((Rel 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ ◡𝐴)
Theorem	cnvct 8983	If a set is countable, so is its converse. (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ (𝐴 ≼ ω → ◡𝐴 ≼ ω)
Theorem	fndmeng 8984	A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐴 ≈ 𝐹)
Theorem	mapsnend 8985	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.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 ↑m {𝐵}) ≈ 𝐴)
Theorem	mapsnen 8986	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.) (Proof shortened by AV, 17-Jul-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ↑m {𝐵}) ≈ 𝐴
Theorem	snmapen 8987	Set exponentiation: a singleton to any set is equinumerous to that singleton. (Contributed by NM, 17-Dec-2003.) (Revised by AV, 17-Jul-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} ↑m 𝐵) ≈ {𝐴})
Theorem	snmapen1 8988	Set exponentiation: a singleton to any set is equinumerous to ordinal 1. (Proposed by BJ, 17-Jul-2022.) (Contributed by AV, 17-Jul-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} ↑m 𝐵) ≈ 1o)
Theorem	map1 8989	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.) (Proof shortened by AV, 17-Jul-2022.)
⊢ (𝐴 ∈ 𝑉 → (1o ↑m 𝐴) ≈ 1o)
Theorem	en2sn 8990	Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.) Avoid ax-pow 5312. (Revised by BTernaryTau, 31-Jul-2024.) Avoid ax-un 7690. (Revised by BTernaryTau, 25-Sep-2024.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵})
Theorem	0fi 8991	The empty set is finite. (Contributed by FL, 14-Jul-2008.) Avoid ax-10 2147, ax-un 7690. (Revised by BTernaryTau, 13-Jan-2025.)
⊢ ∅ ∈ Fin
Theorem	snfi 8992	A singleton is finite. (Contributed by NM, 4-Nov-2002.) (Proof shortened by BTernaryTau, 13-Jan-2025.)
⊢ {𝐴} ∈ Fin
Theorem	fiprc 8993	The class of finite sets is a proper class. (Contributed by Jeff Hankins, 3-Oct-2008.)
⊢ Fin ∉ V
Theorem	unen 8994	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	enrefnn 8995	Equinumerosity is reflexive for finite ordinals, proved without using the Axiom of Power Sets (unlike enrefg 8933). (Contributed by BTernaryTau, 31-Jul-2024.)
⊢ (𝐴 ∈ ω → 𝐴 ≈ 𝐴)
Theorem	en2prd 8996	Two proper unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐷)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ≈ {𝐶, 𝐷})
Theorem	enpr2d 8997	A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-un 7690. (Revised by BTernaryTau, 23-Dec-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o)
Theorem	ssct 8998	Any subset of a countable set is countable. (Contributed by Thierry Arnoux, 31-Jan-2017.) Avoid ax-pow 5312, ax-un 7690. (Revised by BTernaryTau, 7-Dec-2024.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω) → 𝐴 ≼ ω)
Theorem	difsnen 8999	All decrements of a set are equinumerous. (Contributed by Stefan O'Rear, 19-Feb-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵}))
Theorem	domdifsn 9000	Dominance over a set with one element removed. (Contributed by Stefan O'Rear, 19-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.)
⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ (𝐵 ∖ {𝐶}))