P. 91 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9001-9100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	f1oeng 9001	The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1domg 9002	The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004.)
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵))
Theorem	f1oen 9003	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 9004	The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 19-Jun-1998.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵)
Theorem	brsdom 9005	Strict dominance relation, meaning "𝐵 is strictly greater in size than 𝐴". Definition of [Mendelson] p. 255. (Contributed by NM, 25-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵))
Theorem	isfi 9006*	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 9007	Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
⊢ ≈ ⊆ ≼
Theorem	dfdom2 9008	Alternate definition of dominance. (Contributed by NM, 17-Jun-1998.)
⊢ ≼ = ( ≺ ∪ ≈ )
Theorem	endom 9009	Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.)
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵)
Theorem	sdomdom 9010	Strict dominance implies dominance. (Contributed by NM, 10-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵)
Theorem	sdomnen 9011	Strict dominance implies non-equinumerosity. (Contributed by NM, 10-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵)
Theorem	brdom2 9012	Dominance in terms of strict dominance and equinumerosity. Theorem 22(iv) of [Suppes] p. 97. (Contributed by NM, 17-Jun-1998.)
⊢ (𝐴 ≼ 𝐵 ↔ (𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵))
Theorem	bren2 9013	Equinumerosity expressed in terms of dominance and strict dominance. (Contributed by NM, 23-Oct-2004.)
⊢ (𝐴 ≈ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵))
Theorem	enrefg 9014	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴)
Theorem	enref 9015	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ≈ 𝐴
Theorem	eqeng 9016	Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵))
Theorem	domrefg 9017	Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≼ 𝐴)
Theorem	en2d 9018*	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 9019*	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 9020*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 4-Jan-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ V)    &   ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ V)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))    ⇒   ⊢ 𝐴 ≈ 𝐵
Theorem	en3i 9021*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 19-Jul-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)    &   ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶))    ⇒   ⊢ 𝐴 ≈ 𝐵
Theorem	dom2lem 9022*	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 9023*	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 9024*	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 9025*	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 9026*	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 9027	Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ I ⊆ ≈
Theorem	domssl 9028	If 𝐴 is a subset of 𝐵 and 𝐶 dominates 𝐵, then 𝐶 also dominates 𝐴. (Contributed by BTernaryTau, 7-Dec-2024.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	domssr 9029	If 𝐶 is a superset of 𝐵 and 𝐵 dominates 𝐴, then 𝐶 also dominates 𝐴. (Contributed by BTernaryTau, 7-Dec-2024.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐴 ≼ 𝐵) → 𝐴 ≼ 𝐶)
Theorem	ssdomg 9030	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 9031	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 9032	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴)
Theorem	ensym 9033	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
Theorem	ensymi 9034	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    ⇒   ⊢ 𝐵 ≈ 𝐴
Theorem	ensymd 9035	Symmetry of equinumerosity. Deduction form of ensym 9033. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≈ 𝐴)
Theorem	entr 9036	Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)
Theorem	domtr 9037	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 9038	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐵 ≈ 𝐶    ⇒   ⊢ 𝐴 ≈ 𝐶
Theorem	entr2i 9039	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐵 ≈ 𝐶    ⇒   ⊢ 𝐶 ≈ 𝐴
Theorem	entr3i 9040	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐴 ≈ 𝐶    ⇒   ⊢ 𝐵 ≈ 𝐶
Theorem	entr4i 9041	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐶 ≈ 𝐵    ⇒   ⊢ 𝐴 ≈ 𝐶
Theorem	endomtr 9042	Transitivity of equinumerosity and dominance. (Contributed by NM, 7-Jun-1998.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	domentr 9043	Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.)
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	f1imaeng 9044	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 9045	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 9044 does not need ax-rep 5289.) (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉)) → (𝐹 “ 𝐶) ≈ 𝐶)
Theorem	f1imaen3g 9046	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 9044 does not need ax-rep 5289 nor ax-pow 5368.) (Contributed by BTernaryTau, 13-Jan-2025.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ 𝑉) → 𝐶 ≈ (𝐹 “ 𝐶))
Theorem	f1imaen 9047	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 9048	The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.) Avoid ax-pow 5368, ax-un 7745. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)
Theorem	en0OLD 9049	Obsolete version of en0 9048 as of 23-Sep-2024. (Contributed by NM, 27-May-1998.) Avoid ax-pow 5368. (Revised by BTernaryTau, 31-Jul-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)
Theorem	en0ALT 9050	Shorter proof of en0 9048, depending on ax-pow 5368 and ax-un 7745. (Contributed by NM, 27-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)
Theorem	en0r 9051	The empty set is equinumerous only to itself. (Contributed by BTernaryTau, 29-Nov-2024.)
⊢ (∅ ≈ 𝐴 ↔ 𝐴 = ∅)
Theorem	ensn1 9052	A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.) Avoid ax-un 7745. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ≈ 1o
Theorem	ensn1OLD 9053	Obsolete version of ensn1 9052 as of 23-Sep-2024. (Contributed by NM, 4-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ≈ 1o
Theorem	ensn1g 9054	A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ 1o)
Theorem	enpr1g 9055	{𝐴, 𝐴} has only one element. (Contributed by FL, 15-Feb-2010.)
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐴} ≈ 1o)
Theorem	en1 9056*	A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004.) Avoid ax-un 7745. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	en1OLD 9057*	Obsolete version of en1 9056 as of 23-Sep-2024. (Contributed by NM, 25-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	en1b 9058	A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015.) Avoid ax-un 7745. (Revised by BTernaryTau, 24-Sep-2024.)
⊢ (𝐴 ≈ 1o ↔ 𝐴 = {∪ 𝐴})
Theorem	en1bOLD 9059	Obsolete version of en1b 9058 as of 24-Sep-2024. (Contributed by Mario Carneiro, 17-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≈ 1o ↔ 𝐴 = {∪ 𝐴})
Theorem	reuen1 9060*	Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} ≈ 1o)
Theorem	euen1 9061	Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∃!𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≈ 1o)
Theorem	euen1b 9062*	Two ways to express "𝐴 has a unique element". (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ (𝐴 ≈ 1o ↔ ∃!𝑥 𝑥 ∈ 𝐴)
Theorem	en1uniel 9063	A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015.) Avoid ax-un 7745. (Revised by BTernaryTau, 24-Sep-2024.)
⊢ (𝑆 ≈ 1o → ∪ 𝑆 ∈ 𝑆)
Theorem	en1unielOLD 9064	Obsolete version of en1uniel 9063 as of 24-Sep-2024. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑆 ≈ 1o → ∪ 𝑆 ∈ 𝑆)
Theorem	2dom 9065*	A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004.)
⊢ (2o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)
Theorem	fundmen 9066	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 9067	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 17-Sep-2013.)
⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → dom 𝐹 ≈ 𝐹)
Theorem	cnven 9068	A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ ((Rel 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ ◡𝐴)
Theorem	cnvct 9069	If a set is countable, so is its converse. (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ (𝐴 ≼ ω → ◡𝐴 ≼ ω)
Theorem	fndmeng 9070	A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐴 ≈ 𝐹)
Theorem	mapsnend 9071	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 9072	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 9073	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 9074	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 9075	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 9076	Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.) Avoid ax-pow 5368. (Revised by BTernaryTau, 31-Jul-2024.) Avoid ax-un 7745. (Revised by BTernaryTau, 25-Sep-2024.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵})
Theorem	en2snOLD 9077	Obsolete version of en2sn 9076 as of 25-Sep-2024. (Contributed by NM, 9-Nov-2003.) Avoid ax-pow 5368. (Revised by BTernaryTau, 31-Jul-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵})
Theorem	en2snOLDOLD 9078	Obsolete version of en2sn 9076 as of 31-Jul-2024. (Contributed by NM, 9-Nov-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵})
Theorem	0fi 9079	The empty set is finite. (Contributed by FL, 14-Jul-2008.) Avoid ax-10 2129, ax-un 7745. (Revised by BTernaryTau, 13-Jan-2025.)
⊢ ∅ ∈ Fin
Theorem	snfi 9080	A singleton is finite. (Contributed by NM, 4-Nov-2002.) (Proof shortened by BTernaryTau, 13-Jan-2025.)
⊢ {𝐴} ∈ Fin
Theorem	snfiOLD 9081	Obsolete version of snfi 9080 as of 13-Jan-2025. (Contributed by NM, 4-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝐴} ∈ Fin
Theorem	fiprc 9082	The class of finite sets is a proper class. (Contributed by Jeff Hankins, 3-Oct-2008.)
⊢ Fin ∉ V
Theorem	unen 9083	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 9084	Equinumerosity is reflexive for finite ordinals, proved without using the Axiom of Power Sets (unlike enrefg 9014). (Contributed by BTernaryTau, 31-Jul-2024.)
⊢ (𝐴 ∈ ω → 𝐴 ≈ 𝐴)
Theorem	en2prd 9085	Two unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐷)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ≈ {𝐶, 𝐷})
Theorem	enpr2d 9086	A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-un 7745. (Revised by BTernaryTau, 23-Dec-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o)
Theorem	enpr2dOLD 9087	Obsolete version of enpr2d 9086 as of 23-Dec-2024. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o)
Theorem	ssct 9088	Any subset of a countable set is countable. (Contributed by Thierry Arnoux, 31-Jan-2017.) Avoid ax-pow 5368, ax-un 7745. (Revised by BTernaryTau, 7-Dec-2024.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω) → 𝐴 ≼ ω)
Theorem	ssctOLD 9089	Obsolete version of ssct 9088 as of 7-Dec-2024. (Contributed by Thierry Arnoux, 31-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω) → 𝐴 ≼ ω)
Theorem	difsnen 9090	All decrements of a set are equinumerous. (Contributed by Stefan O'Rear, 19-Feb-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵}))
Theorem	domdifsn 9091	Dominance over a set with one element removed. (Contributed by Stefan O'Rear, 19-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.)
⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ (𝐵 ∖ {𝐶}))
Theorem	xpsnen 9092	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 9093	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 9094	One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 1o) ≈ 𝐴)
Theorem	endisj 9095*	Any two sets are equinumerous to two disjoint sets. Exercise 4.39 of [Mendelson] p. 255. (Contributed by NM, 16-Apr-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∃𝑥∃𝑦((𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵) ∧ (𝑥 ∩ 𝑦) = ∅)
Theorem	undom 9096	Dominance law for union. Proposition 4.24(a) of [Mendelson] p. 257. (Contributed by NM, 3-Sep-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) Avoid ax-pow 5368. (Revised by BTernaryTau, 4-Dec-2024.)
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼ (𝐵 ∪ 𝐷))
Theorem	undomOLD 9097	Obsolete version of undom 9096 as of 4-Dec-2024. (Contributed by NM, 3-Sep-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼ (𝐵 ∪ 𝐷))
Theorem	xpcomf1o 9098*	The canonical bijection from (𝐴 × 𝐵) to (𝐵 × 𝐴). (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥})    ⇒   ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴)
Theorem	xpcomco 9099*	Composition with the bijection of xpcomf1o 9098 swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥})    &   ⊢ 𝐺 = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶)    ⇒   ⊢ (𝐺 ∘ 𝐹) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	xpcomen 9100	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    ⇒   ⊢ (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)