P. 80 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7901-8000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dmex 7901	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Jul-2008.)
⊢ 𝐴 ∈ V    ⇒   ⊢ dom 𝐴 ∈ V
Theorem	rnex 7902	The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 7-Jul-2008.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ran 𝐴 ∈ V
Theorem	iprc 7903	The identity function is a proper class. This means, for example, that we cannot use it as a member of the class of continuous functions unless it is restricted to a set, as in idcn 22760. (Contributed by NM, 1-Jan-2007.)
⊢ ¬ I ∈ V
Theorem	resiexg 7904	The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 7216). (Contributed by NM, 13-Jan-2007.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V)
Theorem	imaexg 7905	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by NM, 24-Jul-1995.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)
Theorem	imaex 7906	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by JJ, 24-Sep-2021.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 “ 𝐵) ∈ V
Theorem	exse2 7907	Any set relation is set-like. (Contributed by Mario Carneiro, 22-Jun-2015.)
⊢ (𝑅 ∈ 𝑉 → 𝑅 Se 𝐴)
Theorem	xpexr 7908	If a Cartesian product is a set, one of its components must be a set. (Contributed by NM, 27-Aug-2006.)
⊢ ((𝐴 × 𝐵) ∈ 𝐶 → (𝐴 ∈ V ∨ 𝐵 ∈ V))
Theorem	xpexr2 7909	If a nonempty Cartesian product is a set, so are both of its components. (Contributed by NM, 27-Aug-2006.)
⊢ (((𝐴 × 𝐵) ∈ 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	xpexcnv 7910	A condition where the converse of xpex 7739 holds as well. Corollary 6.9(2) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.)
⊢ ((𝐵 ≠ ∅ ∧ (𝐴 × 𝐵) ∈ V) → 𝐴 ∈ V)
Theorem	soex 7911	If the relation in a strict order is a set, then the base field is also a set. (Contributed by Mario Carneiro, 27-Apr-2015.)
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉) → 𝐴 ∈ V)
Theorem	elxp4 7912	Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp5 7913, elxp6 8008, and elxp7 8009. (Contributed by NM, 17-Feb-2004.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
Theorem	elxp5 7913	Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 7912 when the double intersection does not create class existence problems (caused by int0 4966). (Contributed by NM, 1-Aug-2004.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
Theorem	cnvexg 7914	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 17-Mar-1998.)
⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)
Theorem	cnvex 7915	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 19-Dec-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ◡𝐴 ∈ V
Theorem	relcnvexb 7916	A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007.)
⊢ (Rel 𝑅 → (𝑅 ∈ V ↔ ◡𝑅 ∈ V))
Theorem	f1oexrnex 7917	If the range of a 1-1 onto function is a set, the function itself is a set. (Contributed by AV, 2-Jun-2019.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐹 ∈ V)
Theorem	f1oexbi 7918*	There is a one-to-one onto function from a set to a second set iff there is a one-to-one onto function from the second set to the first set. (Contributed by Alexander van der Vekens, 30-Sep-2018.)
⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 ↔ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴)
Theorem	coexg 7919	The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)
Theorem	coex 7920	The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∘ 𝐵) ∈ V
Theorem	funcnvuni 7921*	The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 6617 for "single-rooted" definition.) (Contributed by NM, 11-Aug-2004.)
⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴)
Theorem	fun11uni 7922*	The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by NM, 11-Aug-2004.)
⊢ (∀𝑓 ∈ 𝐴 ((Fun 𝑓 ∧ Fun ◡𝑓) ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (Fun ∪ 𝐴 ∧ Fun ◡∪ 𝐴))
Theorem	fex2 7923	A function with bounded domain and codomain is a set. This version of fex 7227 is proven without the Axiom of Replacement ax-rep 5285, but depends on ax-un 7724, which is not required for the proof of fex 7227. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)
Theorem	fabexg 7924*	Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008.)
⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V)
Theorem	fabex 7925*	Existence of a set of functions. (Contributed by NM, 3-Dec-2007.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)}    ⇒   ⊢ 𝐹 ∈ V
Theorem	f1oabexg 7926*	The class of all 1-1-onto functions mapping one set to another is a set. (Contributed by Paul Chapman, 25-Feb-2008.)
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐵 ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V)
Theorem	fiunlem 7927*	Lemma for fiun 7928 and f1iun 7929. Formerly part of f1iun 7929. (Contributed by AV, 6-Oct-2023.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
Theorem	fiun 7928*	The union of a chain (with respect to inclusion) of functions is a function. Analogous to f1iun 7929. (Contributed by AV, 6-Oct-2023.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆)
Theorem	f1iun 7929*	The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013.) (Revised by Mario Carneiro, 24-Jun-2015.) (Proof shortened by AV, 5-Nov-2023.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆)
Theorem	fviunfun 7930*	The function value of an indexed union is the value of one of the indexed functions. (Contributed by AV, 4-Nov-2023.)
⊢ 𝑈 = ∪ 𝑖 ∈ 𝐼 (𝐹‘𝑖)    ⇒   ⊢ ((Fun 𝑈 ∧ 𝐽 ∈ 𝐼 ∧ 𝑋 ∈ dom (𝐹‘𝐽)) → (𝑈‘𝑋) = ((𝐹‘𝐽)‘𝑋))
Theorem	ffoss 7931*	Relationship between a mapping and an onto mapping. Figure 38 of [Enderton] p. 145. (Contributed by NM, 10-May-1998.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹:𝐴⟶𝐵 ↔ ∃𝑥(𝐹:𝐴–onto→𝑥 ∧ 𝑥 ⊆ 𝐵))
Theorem	f11o 7932*	Relationship between one-to-one and one-to-one onto function. (Contributed by NM, 4-Apr-1998.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹:𝐴–1-1→𝐵 ↔ ∃𝑥(𝐹:𝐴–1-1-onto→𝑥 ∧ 𝑥 ⊆ 𝐵))
Theorem	resfunexgALT 7933	Alternate proof of resfunexg 7216, shorter but requiring ax-pow 5363 and ax-un 7724. (Contributed by NM, 7-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V)
Theorem	cofunexg 7934	Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∘ 𝐵) ∈ V)
Theorem	cofunex2g 7935	Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007.)
⊢ ((𝐴 ∈ 𝑉 ∧ Fun ◡𝐵) → (𝐴 ∘ 𝐵) ∈ V)
Theorem	fnexALT 7936	Alternate proof of fnex 7218, derived using the Axiom of Replacement in the form of funimaexg 6634. This version uses ax-pow 5363 and ax-un 7724, whereas fnex 7218 does not. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V)
Theorem	funexw 7937	Weak version of funex 7220 that holds without ax-rep 5285. If the domain and codomain of a function exist, so does the function. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ ((Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵 ∧ ran 𝐹 ∈ 𝐶) → 𝐹 ∈ V)
Theorem	mptexw 7938*	Weak version of mptex 7224 that holds without ax-rep 5285. If the domain and codomain of a function given by maps-to notation are sets, the function is a set. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V
Theorem	funrnex 7939	If the domain of a function exists, so does its range. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of funex 7220. (Contributed by NM, 11-Nov-1995.)
⊢ (dom 𝐹 ∈ 𝐵 → (Fun 𝐹 → ran 𝐹 ∈ V))
Theorem	zfrep6 7940*	A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 5299 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version in place of our ax-rep 5285. (Contributed by NM, 10-Oct-2003.)
⊢ (∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑)
Theorem	focdmex 7941	If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004.)
⊢ (𝐴 ∈ 𝐶 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V))
Theorem	f1dmex 7942	If the codomain of a one-to-one function exists, so does its domain. This theorem is equivalent to the Axiom of Replacement ax-rep 5285. (Contributed by NM, 4-Sep-2004.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
Theorem	f1ovv 7943	The codomain/range of a 1-1 onto function is a set iff its domain is a set. (Contributed by AV, 21-Mar-2019.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
Theorem	fvclex 7944*	Existence of the class of values of a set. (Contributed by NM, 9-Nov-1995.)
⊢ 𝐹 ∈ V    ⇒   ⊢ {𝑦 ∣ ∃𝑥 𝑦 = (𝐹‘𝑥)} ∈ V
Theorem	fvresex 7945*	Existence of the class of values of a restricted class. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑦 ∣ ∃𝑥 𝑦 = ((𝐹 ↾ 𝐴)‘𝑥)} ∈ V
Theorem	abrexexg 7946*	Existence of a class abstraction of existentially restricted sets. The class 𝐵 can be thought of as an expression in 𝑥 (which is typically a free variable in the class expression substituted for 𝐵) and the class abstraction appearing in the statement as the class of values 𝐵 as 𝑥 varies through 𝐴. If the "domain" 𝐴 is a set, then the abstraction is also a set. Therefore, this statement is a kind of Replacement. This can be seen by tracing back through the path axrep6g 5293, axrep6 5292, ax-rep 5285. See also abrexex2g 7950. There are partial converses under additional conditions, see for instance abnexg 7742. (Contributed by NM, 3-Nov-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) Avoid ax-10 2137, ax-11 2154, ax-12 2171, ax-pr 5427, ax-un 7724 and shorten proof. (Revised by SN, 11-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
Theorem	abrexexgOLD 7947*	Obsolete version of abrexexg 7946 as of 11-Dec-2024. EDITORIAL: Comment kept since the line of equivalences to ax-rep 5285 is different. Existence of a class abstraction of existentially restricted sets. The class 𝐵 can be thought of as an expression in 𝑥 (which is typically a free variable in the class expression substituted for 𝐵) and the class abstraction appearing in the statement as the class of values 𝐵 as 𝑥 varies through 𝐴. If the "domain" 𝐴 is a set, then the abstraction is also a set. Therefore, this statement is a kind of Replacement. This can be seen by tracing back through the path mptexg 7222, funex 7220, fnex 7218, resfunexg 7216, and funimaexg 6634. See also abrexex2g 7950. There are partial converses under additional conditions, see for instance abnexg 7742. (Contributed by NM, 3-Nov-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
Theorem	abrexex 7948*	Existence of a class abstraction of existentially restricted sets. See the comment of abrexexg 7946. See also abrexex2 7955. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V
Theorem	iunexg 7949*	The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵. (Contributed by NM, 23-Mar-2006.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
Theorem	abrexex2g 7950*	Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V)
Theorem	opabex3d 7951*	Existence of an ordered pair abstraction, deduction version. (Contributed by Alexander van der Vekens, 19-Oct-2017.) (Revised by AV, 9-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝜓} ∈ V)    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} ∈ V)
Theorem	opabex3rd 7952*	Existence of an ordered pair abstraction if the second components are elements of a set. (Contributed by AV, 17-Sep-2023.) (Revised by AV, 9-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → {𝑥 ∣ 𝜓} ∈ V)    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} ∈ V)
Theorem	opabex3 7953*	Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → {𝑦 ∣ 𝜑} ∈ V)    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V
Theorem	iunex 7954*	The existence of an indexed union. 𝑥 is normally a free-variable parameter in the class expression substituted for 𝐵, which can be read informally as 𝐵(𝑥). (Contributed by NM, 13-Oct-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V
Theorem	abrexex2 7955*	Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥 and 𝑦. See also abrexex 7948. (Contributed by NM, 12-Sep-2004.)
⊢ 𝐴 ∈ V    &   ⊢ {𝑦 ∣ 𝜑} ∈ V    ⇒   ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V
Theorem	abexssex 7956*	Existence of a class abstraction with an existentially quantified expression. Both 𝑥 and 𝑦 can be free in 𝜑. (Contributed by NM, 29-Jul-2006.)
⊢ 𝐴 ∈ V    &   ⊢ {𝑦 ∣ 𝜑} ∈ V    ⇒   ⊢ {𝑦 ∣ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝜑)} ∈ V
Theorem	abexex 7957*	A condition where a class abstraction continues to exist after its wff is existentially quantified. (Contributed by NM, 4-Mar-2007.)
⊢ 𝐴 ∈ V    &   ⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ {𝑦 ∣ 𝜑} ∈ V    ⇒   ⊢ {𝑦 ∣ ∃𝑥𝜑} ∈ V
Theorem	f1oweALT 7958*	Alternate proof of f1owe 7349, more direct since not using the isomorphism predicate, but requiring ax-un 7724. (Contributed by NM, 4-Mar-1997.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)}    ⇒   ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴))
Theorem	wemoiso 7959*	Thus, there is at most one isomorphism between any two well-ordered sets. TODO: Shorten finnisoeu 10107. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ (𝑅 We 𝐴 → ∃*𝑓 𝑓 Isom 𝑅, 𝑆 (𝐴, 𝐵))
Theorem	wemoiso2 7960*	Thus, there is at most one isomorphism between any two well-ordered sets. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ (𝑆 We 𝐵 → ∃*𝑓 𝑓 Isom 𝑅, 𝑆 (𝐴, 𝐵))
Theorem	oprabexd 7961*	Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by AV, 9-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑧𝜓)    &   ⊢ (𝜑 → 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)})    ⇒   ⊢ (𝜑 → 𝐹 ∈ V)
Theorem	oprabex 7962*	Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃*𝑧𝜑)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)}    ⇒   ⊢ 𝐹 ∈ V
Theorem	oprabex3 7963*	Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004.)
⊢ 𝐻 ∈ V    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}    ⇒   ⊢ 𝐹 ∈ V
Theorem	oprabrexex2 7964*	Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.)
⊢ 𝐴 ∈ V    &   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ∈ V    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑤 ∈ 𝐴 𝜑} ∈ V
Theorem	ab2rexex 7965*	Existence of a class abstraction of existentially restricted sets. Variables 𝑥 and 𝑦 are normally free-variable parameters in the class expression substituted for 𝐶, which can be thought of as 𝐶(𝑥, 𝑦). See comments for abrexex 7948. (Contributed by NM, 20-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} ∈ V
Theorem	ab2rexex2 7966*	Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥, 𝑦, and 𝑧. Compare abrexex2 7955. (Contributed by NM, 20-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ {𝑧 ∣ 𝜑} ∈ V    ⇒   ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} ∈ V
Theorem	xpexgALT 7967	Alternate proof of xpexg 7736 requiring Replacement (ax-rep 5285) but not Power Set (ax-pow 5363). (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
Theorem	offval3 7968*	General value of (𝐹 ∘f 𝑅𝐺) with no assumptions on functionality of 𝐹 and 𝐺. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))))
Theorem	offres 7969	Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘f 𝑅𝐺) ↾ 𝐷) = ((𝐹 ↾ 𝐷) ∘f 𝑅(𝐺 ↾ 𝐷)))
Theorem	ofmres 7970*	Equivalent expressions for a restriction of the function operation map. Unlike ∘f 𝑅 which is a proper class, ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) can be a set by ofmresex 7971, allowing it to be used as a function or structure argument. By ofmresval 7685, the restricted operation map values are the same as the original values, allowing theorems for ∘f 𝑅 to be reused. (Contributed by NM, 20-Oct-2014.)
⊢ ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) = (𝑓 ∈ 𝐴, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘f 𝑅𝑔))
Theorem	ofmresex 7971	Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) ∈ V)
2.4.8  First and second members of an ordered pair
Syntax	c1st 7972	Extend the definition of a class to include the first member an ordered pair function.
class 1st
Syntax	c2nd 7973	Extend the definition of a class to include the second member an ordered pair function.
class 2nd
Definition	df-1st 7974	Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 7982 proves that it does this. For example, (1st ‘⟨3, 4⟩) = 3. Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 6224 and op1stb 5471). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
Definition	df-2nd 7975	Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 7983 proves that it does this. For example, (2nd ‘⟨3, 4⟩) = 4. Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 6227 and op2ndb 6226). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥})
Theorem	1stval 7976	The value of the function that extracts the first member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (1st ‘𝐴) = ∪ dom {𝐴}
Theorem	2ndval 7977	The value of the function that extracts the second member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (2nd ‘𝐴) = ∪ ran {𝐴}
Theorem	1stnpr 7978	Value of the first-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ (¬ 𝐴 ∈ (V × V) → (1st ‘𝐴) = ∅)
Theorem	2ndnpr 7979	Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ (¬ 𝐴 ∈ (V × V) → (2nd ‘𝐴) = ∅)
Theorem	1st0 7980	The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
⊢ (1st ‘∅) = ∅
Theorem	2nd0 7981	The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
⊢ (2nd ‘∅) = ∅
Theorem	op1st 7982	Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴
Theorem	op2nd 7983	Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
Theorem	op1std 7984	Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1st ‘𝐶) = 𝐴)
Theorem	op2ndd 7985	Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = 𝐵)
Theorem	op1stg 7986	Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)
Theorem	op2ndg 7987	Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)
Theorem	ot1stg 7988	Extract the first member of an ordered triple. (Due to infrequent usage, it isn't worthwhile at this point to define special extractors for triples, so we reuse the ordered pair extractors for ot1stg 7988, ot2ndg 7989, ot3rdg 7990.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (1st ‘(1st ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐴)
Theorem	ot2ndg 7989	Extract the second member of an ordered triple. (See ot1stg 7988 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2nd ‘(1st ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐵)
Theorem	ot3rdg 7990	Extract the third member of an ordered triple. (See ot1stg 7988 comment.) (Contributed by NM, 3-Apr-2015.)
⊢ (𝐶 ∈ 𝑉 → (2nd ‘⟨𝐴, 𝐵, 𝐶⟩) = 𝐶)
Theorem	1stval2 7991	Alternate value of the function that extracts the first member of an ordered pair. Definition 5.13 (i) of [Monk1] p. 52. (Contributed by NM, 18-Aug-2006.)
⊢ (𝐴 ∈ (V × V) → (1st ‘𝐴) = ∩ ∩ 𝐴)
Theorem	2ndval2 7992	Alternate value of the function that extracts the second member of an ordered pair. Definition 5.13 (ii) of [Monk1] p. 52. (Contributed by NM, 18-Aug-2006.)
⊢ (𝐴 ∈ (V × V) → (2nd ‘𝐴) = ∩ ∩ ∩ ◡{𝐴})
Theorem	oteqimp 7993	The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
⊢ (𝑇 = ⟨𝐴, 𝐵, 𝐶⟩ → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = 𝐵 ∧ (2nd ‘𝑇) = 𝐶)))
Theorem	fo1st 7994	The 1st function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ 1st :V–onto→V
Theorem	fo2nd 7995	The 2nd function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ 2nd :V–onto→V
Theorem	br1steqg 7996	Uniqueness condition for the binary relation 1st. (Contributed by Scott Fenton, 2-Jul-2020.) Revised to remove sethood hypothesis on 𝐶. (Revised by Peter Mazsa, 17-Jan-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩1st 𝐶 ↔ 𝐶 = 𝐴))
Theorem	br2ndeqg 7997	Uniqueness condition for the binary relation 2nd. (Contributed by Scott Fenton, 2-Jul-2020.) Revised to remove sethood hypothesis on 𝐶. (Revised by Peter Mazsa, 17-Jan-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩2nd 𝐶 ↔ 𝐶 = 𝐵))
Theorem	f1stres 7998	Mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 11-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐴
Theorem	f2ndres 7999	Mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 7-Aug-2006.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (2nd ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐵
Theorem	fo1stres 8000	Onto mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 14-Dec-2008.)
⊢ (𝐵 ≠ ∅ → (1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)–onto→𝐴)