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	fdiagfn 8901*	Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑m 𝐼))
Theorem	fvdiagfn 8902*	Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (𝐼 × {𝑋}))
Theorem	mapsnconst 8903	Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    ⇒   ⊢ (𝐹 ∈ (𝐵 ↑m 𝑆) → 𝐹 = (𝑆 × {(𝐹‘𝑋)}))
Theorem	mapsncnv 8904*	Expression for the inverse of the canonical map between a set and its set of singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑m 𝑆) ↦ (𝑥‘𝑋))    ⇒   ⊢ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦}))
Theorem	mapsnf1o2 8905*	Explicit bijection between a set and its singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑m 𝑆) ↦ (𝑥‘𝑋))    ⇒   ⊢ 𝐹:(𝐵 ↑m 𝑆)–1-1-onto→𝐵
Theorem	mapsnf1o3 8906*	Explicit bijection in the reverse of mapsnf1o2 8905. (Contributed by Stefan O'Rear, 24-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦}))    ⇒   ⊢ 𝐹:𝐵–1-1-onto→(𝐵 ↑m 𝑆)
Theorem	ralxpmap 8907*	Quantification over functions in terms of quantification over values and punctured functions. (Contributed by Stefan O'Rear, 27-Feb-2015.) (Revised by Stefan O'Rear, 5-May-2015.)
⊢ (𝑓 = (𝑔 ∪ {⟨𝐽, 𝑦⟩}) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐽 ∈ 𝑇 → (∀𝑓 ∈ (𝑆 ↑m 𝑇)𝜑 ↔ ∀𝑦 ∈ 𝑆 ∀𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝜓))
2.4.28  Infinite Cartesian products
Syntax	cixp 8908	Extend class notation to include infinite Cartesian products.
class X𝑥 ∈ 𝐴 𝐵
Definition	df-ixp 8909*	Definition of infinite Cartesian product of [Enderton] p. 54. Enderton uses a bold "X" with 𝑥 ∈ 𝐴 written underneath or as a subscript, as does Stoll p. 47. Some books use a capital pi, but we will reserve that notation for products of numbers. Usually 𝐵 represents a class expression containing 𝑥 free and thus can be thought of as 𝐵(𝑥). Normally, 𝑥 is not free in 𝐴, although this is not a requirement of the definition. (Contributed by NM, 28-Sep-2006.)
⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)}
Theorem	dfixp 8910*	Eliminate the expression {𝑥 ∣ 𝑥 ∈ 𝐴} in df-ixp 8909, under the assumption that 𝐴 and 𝑥 are disjoint. This way, we can say that 𝑥 is bound in X𝑥 ∈ 𝐴𝐵 even if it appears free in 𝐴. (Contributed by Mario Carneiro, 12-Aug-2016.)
⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)}
Theorem	ixpsnval 8911*	The value of an infinite Cartesian product with a singleton. (Contributed by AV, 3-Dec-2018.)
⊢ (𝑋 ∈ 𝑉 → X𝑥 ∈ {𝑋}𝐵 = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌𝐵)})
Theorem	elixp2 8912*	Membership in an infinite Cartesian product. See df-ixp 8909 for discussion of the notation. (Contributed by NM, 28-Sep-2006.)
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	fvixp 8913*	Projection of a factor of an indexed Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)    ⇒   ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐷)
Theorem	ixpfn 8914*	A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-May-2014.)
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹 Fn 𝐴)
Theorem	elixp 8915*	Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	elixpconst 8916*	Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by NM, 12-Apr-2008.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵)
Theorem	ixpconstg 8917*	Infinite Cartesian product of a constant 𝐵. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑m 𝐴))
Theorem	ixpconst 8918*	Infinite Cartesian product of a constant 𝐵. (Contributed by NM, 28-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑m 𝐴)
Theorem	ixpeq1 8919*	Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶)
Theorem	ixpeq1d 8920*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶)
Theorem	ss2ixp 8921	Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2 8922	Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2dva 8923*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2dv 8924*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	cbvixp 8925*	Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶
Theorem	cbvixpv 8926*	Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶
Theorem	nfixpw 8927*	Bound-variable hypothesis builder for indexed Cartesian product. Version of nfixp 8928 with a disjoint variable condition, which does not require ax-13 2403. (Contributed by Mario Carneiro, 15-Oct-2016.) Avoid ax-13 2403. (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦X𝑥 ∈ 𝐴 𝐵
Theorem	nfixp 8928	Bound-variable hypothesis builder for indexed Cartesian product. Usage of this theorem is discouraged because it depends on ax-13 2403. Use the weaker nfixpw 8927 when possible. (Contributed by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦X𝑥 ∈ 𝐴 𝐵
Theorem	nfixp1 8929	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.)
⊢ Ⅎ𝑥X𝑥 ∈ 𝐴 𝐵
Theorem	ixpprc 8930*	A cartesian product of proper-class many sets is empty, because any function in the cartesian product has to be a set with domain 𝐴, which is not possible for a proper class domain. (Contributed by Mario Carneiro, 25-Jan-2015.)
⊢ (¬ 𝐴 ∈ V → X𝑥 ∈ 𝐴 𝐵 = ∅)
Theorem	ixpf 8931*	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.)
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹:𝐴⟶∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	uniixp 8932*	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.)
⊢ ∪ X𝑥 ∈ 𝐴 𝐵 ⊆ (𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ixpexg 8933*	The existence of an infinite Cartesian product. 𝑥 is normally a free-variable parameter in 𝐵. Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006.) (Revised by Mario Carneiro, 25-Jan-2015.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ∈ V)
Theorem	ixpin 8934*	The intersection of two infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ X𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (X𝑥 ∈ 𝐴 𝐵 ∩ X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpiin 8935*	The indexed intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 6-Feb-2015.)
⊢ (𝐵 ≠ ∅ → X𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpint 8936*	The intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ (𝐵 ≠ ∅ → X𝑥 ∈ 𝐴 ∩ 𝐵 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝑦)
Theorem	ixp0x 8937	An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007.)
⊢ X𝑥 ∈ ∅ 𝐴 = {∅}
Theorem	ixpssmap2g 8938*	An infinite Cartesian product is a subset of set exponentiation. This version of ixpssmapg 8939 avoids ax-rep 5236. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴))
Theorem	ixpssmapg 8939*	An infinite Cartesian product is a subset of set exponentiation. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴))
Theorem	0elixp 8940	Membership of the empty set in an infinite Cartesian product. (Contributed by Steve Rodriguez, 29-Sep-2006.)
⊢ ∅ ∈ X𝑥 ∈ ∅ 𝐴
Theorem	ixpn0 8941	The infinite Cartesian product of a family 𝐵(𝑥) with an empty member is empty. The converse of this theorem is equivalent to the Axiom of Choice, see ac9 10489. (Contributed by Mario Carneiro, 22-Jun-2016.)
⊢ (X𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∀𝑥 ∈ 𝐴 𝐵 ≠ ∅)
Theorem	ixp0 8942	The infinite Cartesian product of a family 𝐵(𝑥) with an empty member is empty. The converse of this theorem is equivalent to the Axiom of Choice, see ac9 10489. (Contributed by NM, 1-Oct-2006.) (Proof shortened by Mario Carneiro, 22-Jun-2016.)
⊢ (∃𝑥 ∈ 𝐴 𝐵 = ∅ → X𝑥 ∈ 𝐴 𝐵 = ∅)
Theorem	ixpssmap 8943*	An infinite Cartesian product is a subset of set exponentiation. Remark in [Enderton] p. 54. (Contributed by NM, 28-Sep-2006.)
⊢ 𝐵 ∈ V    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴)
Theorem	resixp 8944*	Restriction of an element of an infinite Cartesian product. (Contributed by FL, 7-Nov-2011.) (Proof shortened by Mario Carneiro, 31-May-2014.)
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X𝑥 ∈ 𝐴 𝐶) → (𝐹 ↾ 𝐵) ∈ X𝑥 ∈ 𝐵 𝐶)
Theorem	undifixp 8945*	Union of two projections of a cartesian product. (Contributed by FL, 7-Nov-2011.)
⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶)
Theorem	mptelixpg 8946*	Condition for an explicit member of an indexed product. (Contributed by Stefan O'Rear, 4-Jan-2015.)
⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
Theorem	resixpfo 8947*	Restriction of elements of an infinite Cartesian product creates a surjection, if the original Cartesian product is nonempty. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ 𝐹 = (𝑓 ∈ X𝑥 ∈ 𝐴 𝐶 ↦ (𝑓 ↾ 𝐵))    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ X𝑥 ∈ 𝐴 𝐶 ≠ ∅) → 𝐹:X𝑥 ∈ 𝐴 𝐶–onto→X𝑥 ∈ 𝐵 𝐶)
Theorem	elixpsn 8948*	Membership in a class of singleton functions. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ {𝐴}𝐵 ↔ ∃𝑦 ∈ 𝐵 𝐹 = {⟨𝐴, 𝑦⟩}))
Theorem	ixpsnf1o 8949*	A bijection between a class and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ({𝐼} × {𝑥}))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐹:𝐴–1-1-onto→X𝑦 ∈ {𝐼}𝐴)
Theorem	mapsnf1o 8950*	A bijection between a set and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ({𝐼} × {𝑥}))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐴–1-1-onto→(𝐴 ↑m {𝐼}))
Theorem	boxriin 8951*	A rectangular subset of a rectangular set can be recovered as the relative intersection of single-axis restrictions. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (∀𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 → X𝑥 ∈ 𝐼 𝐴 = (X𝑥 ∈ 𝐼 𝐵 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐴, 𝐵)))
Theorem	boxcutc 8952*	The relative complement of a box set restricted on one axis. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) → (X𝑘 ∈ 𝐴 𝐵 ∖ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵)) = X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵))
2.4.29  Equinumerosity
Syntax	cen 8953	Extend class definition to include the equinumerosity relation ("approximately equals" symbol)
class ≈
Syntax	cdom 8954	Extend class definition to include the dominance relation (curly "less than or equal to")
class ≼
Syntax	csdm 8955	Extend class definition to include the strict dominance relation (curly less-than)
class ≺
Syntax	cfn 8956	Extend class definition to include the class of all finite sets.
class Fin
Definition	df-en 8957*	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 8966. (Contributed by NM, 28-Mar-1998.)
⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦}
Definition	df-dom 8958*	Define the dominance relation. For an alternate definition see dfdom2 8988. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 8970 and domen 8971. (Contributed by NM, 28-Mar-1998.)
⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦}
Definition	df-sdom 8959	Define the strict dominance relation. Alternate possible definitions are derived as brsdom 8984 and brsdom2 9103. Definition 3 of [Suppes] p. 97. (Contributed by NM, 31-Mar-1998.)
⊢ ≺ = ( ≼ ∖ ≈ )
Definition	df-fin 8960*	Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our "𝑎 ∈ Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 9624. If we accept Infinity, we can also express 𝐴 ∈ Fin by 𝐴 ≺ ω (Theorem isfinite 9635.) (Contributed by NM, 22-Aug-2008.)
⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦}
Theorem	relen 8961	Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
⊢ Rel ≈
Theorem	reldom 8962	Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
⊢ Rel ≼
Theorem	relsdom 8963	Strict dominance is a relation. (Contributed by NM, 31-Mar-1998.)
⊢ Rel ≺
Theorem	encv 8964	If two classes are equinumerous, both classes are sets. (Contributed by AV, 21-Mar-2019.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	breng 8965*	Equinumerosity relation. This variation of bren 8966 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of bren 8966. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
Theorem	bren 8966*	Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8965 as an intermediate result. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)
Theorem	brdom2g 8967*	Dominance relation. This variation of brdomg 8968 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of brdomg 8968. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
Theorem	brdomg 8968*	Dominance relation. (Contributed by NM, 15-Jun-1998.) Extract brdom2g 8967 as an intermediate result. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
Theorem	brdomi 8969*	Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.) Avoid ax-un 7740. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵)
Theorem	brdom 8970*	Dominance relation. (Contributed by NM, 15-Jun-1998.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)
Theorem	domen 8971*	Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146. (Contributed by NM, 15-Jun-1998.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))
Theorem	domeng 8972*	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 8973	A countable set is a set. (Contributed by Thierry Arnoux, 29-Dec-2016.) (Proof shortened by Jim Kingdon, 13-Mar-2023.)
⊢ (𝐴 ≼ ω → 𝐴 ∈ V)
Theorem	f1oen4g 8974	The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng 8980 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 8975	The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg 8981 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 8976	The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng 8980 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 8977	The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg 8981 does not require the Axiom of Replacement nor the Axiom of Power Sets. (Contributed by BTernaryTau, 9-Sep-2024.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
Theorem	f1oen2g 8978	The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 8980 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1dom2g 8979	The domain of a one-to-one function is dominated by its codomain. This variation of f1domg 8981 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 8980	The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1domg 8981	The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004.)
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵))
Theorem	f1oen 8982	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 8983	The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 19-Jun-1998.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵)
Theorem	brsdom 8984	Strict dominance relation, meaning "𝐵 is strictly greater in size than 𝐴". Definition of [Mendelson] p. 255. (Contributed by NM, 25-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵))
Theorem	isfi 8985*	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 8986	Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.) (Proof shortened by TM, 10-Feb-2026.)
⊢ ≈ ⊆ ≼
Theorem	enssdomOLD 8987	Obsolete version of enssdom 8986 as of 10-Feb-2026. (Contributed by NM, 31-Mar-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ≈ ⊆ ≼
Theorem	dfdom2 8988	Alternate definition of dominance. (Contributed by NM, 17-Jun-1998.)
⊢ ≼ = ( ≺ ∪ ≈ )
Theorem	endom 8989	Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.)
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵)
Theorem	sdomdom 8990	Strict dominance implies dominance. (Contributed by NM, 10-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵)
Theorem	sdomnen 8991	Strict dominance implies non-equinumerosity. (Contributed by NM, 10-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵)
Theorem	brdom2 8992	Dominance in terms of strict dominance and equinumerosity. Theorem 22(iv) of [Suppes] p. 97. (Contributed by NM, 17-Jun-1998.)
⊢ (𝐴 ≼ 𝐵 ↔ (𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵))
Theorem	bren2 8993	Equinumerosity expressed in terms of dominance and strict dominance. (Contributed by NM, 23-Oct-2004.)
⊢ (𝐴 ≈ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵))
Theorem	enrefg 8994	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴)
Theorem	enref 8995	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ≈ 𝐴
Theorem	eqeng 8996	Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵))
Theorem	domrefg 8997	Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≼ 𝐴)
Theorem	en2d 8998*	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 8999*	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 9000*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 4-Jan-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ V)    &   ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ V)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))    ⇒   ⊢ 𝐴 ≈ 𝐵