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	dmfexALT 7901	Alternate proof of dmfex 7898: shorter but using ax-rep 5239. (Contributed by NM, 27-Aug-2006.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) (Proof shortened by AV, 23-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐹 ∈ 𝐶 ∧ 𝐹:𝐴⟶𝐵) → 𝐴 ∈ V)
Theorem	dmex 7902	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 7903	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 7904	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 23379. (Contributed by NM, 1-Jan-2007.)
⊢ ¬ I ∈ V
Theorem	resiexg 7905	The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 7211). (Contributed by NM, 13-Jan-2007.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V)
Theorem	imaexg 7906	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by NM, 24-Jul-1995.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)
Theorem	imaex 7907	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by JJ, 24-Sep-2021.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 “ 𝐵) ∈ V
Theorem	rnexd 7908	The range of a set is a set. Deduction version of rnexd 7908. (Contributed by Thierry Arnoux, 14-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ran 𝐴 ∈ V)
Theorem	imaexd 7909	The image of a set is a set. Deduction version of imaexg 7906. (Contributed by Thierry Arnoux, 14-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐵) ∈ V)
Theorem	exse2 7910	Any set relation is set-like. (Contributed by Mario Carneiro, 22-Jun-2015.)
⊢ (𝑅 ∈ 𝑉 → 𝑅 Se 𝐴)
Theorem	xpexr 7911	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 7912	If a nonempty Cartesian product is a set, so are both of its components. (Contributed by NM, 27-Aug-2006.)
⊢ (((𝐴 × 𝐵) ∈ 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	xpexcnv 7913	A condition where the converse of xpex 7748 holds as well. Corollary 6.9(2) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.)
⊢ ((𝐵 ≠ ∅ ∧ (𝐴 × 𝐵) ∈ V) → 𝐴 ∈ V)
Theorem	soex 7914	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 7915	Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp5 7916, elxp6 8016, and elxp7 8017. (Contributed by NM, 17-Feb-2004.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
Theorem	elxp5 7916	Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 7915 when the double intersection does not create class existence problems (caused by int0 4928). (Contributed by NM, 1-Aug-2004.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
Theorem	cnvexg 7917	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 7918	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 7919	A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007.)
⊢ (Rel 𝑅 → (𝑅 ∈ V ↔ ◡𝑅 ∈ V))
Theorem	f1oexrnex 7920	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 7921*	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 7922	The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)
Theorem	coex 7923	The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∘ 𝐵) ∈ V
Theorem	coexd 7924	The composition of two sets is a set. (Contributed by SN, 7-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐵) ∈ V)
Theorem	funcnvuni 7925*	The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 6602 for "single-rooted" definition.) (Contributed by NM, 11-Aug-2004.)
⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴)
Theorem	fun11uni 7926*	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	resf1extb 7927	Extension of an injection which is a restriction of a function. (Contributed by AV, 3-Oct-2025.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ∈ (𝐴 ∖ 𝐶) ∧ 𝐶 ⊆ 𝐴) → (((𝐹 ↾ 𝐶):𝐶–1-1→𝐵 ∧ (𝐹‘𝑋) ∉ (𝐹 “ 𝐶)) ↔ (𝐹 ↾ (𝐶 ∪ {𝑋})):(𝐶 ∪ {𝑋})–1-1→𝐵))
Theorem	resf1ext2b 7928	Extension of an injection which is a restriction of a function. (Contributed by AV, 3-Oct-2025.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ∈ (𝐴 ∖ 𝐶) ∧ 𝐶 ⊆ 𝐴) → ((Fun ◡(𝐹 ↾ 𝐶) ∧ (𝐹‘𝑋) ∉ (𝐹 “ 𝐶)) ↔ Fun ◡(𝐹 ↾ (𝐶 ∪ {𝑋}))))
Theorem	fex2 7929	A function with bounded domain and codomain is a set. This version of fex 7222 is proven without the Axiom of Replacement ax-rep 5239, but depends on ax-un 7730, which is not required for the proof of fex 7222. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)
Theorem	fabexd 7930*	Existence of a set of functions. In contrast to fabex 7932 or fabexg 7931, the condition in the class abstraction does not contain the function explicitly, but the function can be derived from it. Therefore, this theorem is also applicable for more special functions like one-to-one, onto or one-to-one onto functions. (Contributed by AV, 20-May-2025.)
⊢ ((𝜑 ∧ 𝜓) → 𝑓:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑊)    ⇒   ⊢ (𝜑 → {𝑓 ∣ 𝜓} ∈ V)
Theorem	fabexg 7931*	Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008.) (Proof shortened by AV, 9-Jun-2025.)
⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V)
Theorem	fabex 7932*	Existence of a set of functions. (Contributed by NM, 3-Dec-2007.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)}    ⇒   ⊢ 𝐹 ∈ V
Theorem	mapex 7933*	The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of [Kunen] p. 31. (Contributed by Raph Levien, 4-Dec-2003.) (Proof shortened by AV, 16-Jun-2025.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V)
Theorem	f1oabexg 7934*	The class of all 1-1-onto functions mapping one set to another is a set. (Contributed by Paul Chapman, 25-Feb-2008.) (Proof shortened by AV, 9-Jun-2025.)
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐵 ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V)
Theorem	fiunlem 7935*	Lemma for fiun 7936 and f1iun 7937. Formerly part of f1iun 7937. (Contributed by AV, 6-Oct-2023.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
Theorem	fiun 7936*	The union of a chain (with respect to inclusion) of functions is a function. Analogous to f1iun 7937. (Contributed by AV, 6-Oct-2023.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆)
Theorem	f1iun 7937*	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 7938*	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 7939*	Relationship between a mapping and an onto mapping. Figure 38 of [Enderton] p. 145. (Contributed by NM, 10-May-1998.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹:𝐴⟶𝐵 ↔ ∃𝑥(𝐹:𝐴–onto→𝑥 ∧ 𝑥 ⊆ 𝐵))
Theorem	f11o 7940*	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 7941	Alternate proof of resfunexg 7211, shorter but requiring ax-pow 5334 and ax-un 7730. (Contributed by NM, 7-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V)
Theorem	cofunexg 7942	Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∘ 𝐵) ∈ V)
Theorem	cofunex2g 7943	Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007.)
⊢ ((𝐴 ∈ 𝑉 ∧ Fun ◡𝐵) → (𝐴 ∘ 𝐵) ∈ V)
Theorem	fnexALT 7944	Alternate proof of fnex 7213, derived using the Axiom of Replacement in the form of funimaexg 6620. This version uses ax-pow 5334 and ax-un 7730, whereas fnex 7213 does not. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V)
Theorem	funexw 7945	Weak version of funex 7215 that holds without ax-rep 5239. 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 7946*	Weak version of mptex 7219 that holds without ax-rep 5239. 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 7947	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 7215. (Contributed by NM, 11-Nov-1995.)
⊢ (dom 𝐹 ∈ 𝐵 → (Fun 𝐹 → ran 𝐹 ∈ V))
Theorem	zfrep6OLD 7948*	Obsolete proof of zfrep6 5251 as of 5-Apr-2026. (Contributed by NM, 10-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑)
Theorem	focdmex 7949	If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004.)
⊢ (𝐴 ∈ 𝐶 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V))
Theorem	f1dmex 7950	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 5239. (Contributed by NM, 4-Sep-2004.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
Theorem	f1ovv 7951	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 7952*	Existence of the class of values of a set. (Contributed by NM, 9-Nov-1995.)
⊢ 𝐹 ∈ V    ⇒   ⊢ {𝑦 ∣ ∃𝑥 𝑦 = (𝐹‘𝑥)} ∈ V
Theorem	fvresex 7953*	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 7954*	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 5252, axrep6 5248, ax-rep 5239. See also abrexex2g 7957. There are partial converses under additional conditions, see for instance abnexg 7751. (Contributed by NM, 3-Nov-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) Avoid ax-10 2182, ax-11 2198, ax-12 2219, ax-pr 5402, ax-un 7730 and shorten proof. (Revised by SN, 11-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
Theorem	abrexex 7955*	Existence of a class abstraction of existentially restricted sets. See the comment of abrexexg 7954. See also abrexex2 7962. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V
Theorem	iunexg 7956*	The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵. (Contributed by NM, 23-Mar-2006.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
Theorem	abrexex2g 7957*	Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V)
Theorem	opabex3d 7958*	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 7959*	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 7960*	Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → {𝑦 ∣ 𝜑} ∈ V)    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V
Theorem	iunex 7961*	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 7962*	Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥 and 𝑦. See also abrexex 7955. (Contributed by NM, 12-Sep-2004.)
⊢ 𝐴 ∈ V    &   ⊢ {𝑦 ∣ 𝜑} ∈ V    ⇒   ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V
Theorem	abexssex 7963*	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 7964*	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 7965*	Alternate proof of f1owe 7349, more direct since not using the isomorphism predicate, but requiring ax-un 7730. (Contributed by NM, 4-Mar-1997.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)}    ⇒   ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴))
Theorem	wemoiso 7966*	Thus, there is at most one isomorphism between any two well-ordered sets. TODO: Shorten finnisoeu 10093. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ (𝑅 We 𝐴 → ∃*𝑓 𝑓 Isom 𝑅, 𝑆 (𝐴, 𝐵))
Theorem	wemoiso2 7967*	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 7968*	Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by AV, 9-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑧𝜓)    &   ⊢ (𝜑 → 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)})    ⇒   ⊢ (𝜑 → 𝐹 ∈ V)
Theorem	oprabex 7969*	Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃*𝑧𝜑)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)}    ⇒   ⊢ 𝐹 ∈ V
Theorem	oprabex3 7970*	Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004.)
⊢ 𝐻 ∈ V    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}    ⇒   ⊢ 𝐹 ∈ V
Theorem	oprabrexex2 7971*	Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.)
⊢ 𝐴 ∈ V    &   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ∈ V    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑤 ∈ 𝐴 𝜑} ∈ V
Theorem	ab2rexex 7972*	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 7955. (Contributed by NM, 20-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} ∈ V
Theorem	ab2rexex2 7973*	Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥, 𝑦, and 𝑧. Compare abrexex2 7962. (Contributed by NM, 20-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ {𝑧 ∣ 𝜑} ∈ V    ⇒   ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} ∈ V
Theorem	xpexgALT 7974	Alternate proof of xpexg 7745 requiring Replacement (ax-rep 5239) but not Power Set (ax-pow 5334). (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
Theorem	offval3 7975*	General value of (𝐹 ∘f 𝑅𝐺) with no assumptions on functionality of 𝐹 and 𝐺. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))))
Theorem	offres 7976	Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘f 𝑅𝐺) ↾ 𝐷) = ((𝐹 ↾ 𝐷) ∘f 𝑅(𝐺 ↾ 𝐷)))
Theorem	ofmres 7977*	Equivalent expressions for a restriction of the function operation map. Unlike ∘f 𝑅 which is a proper class, ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) can be a set by ofmresex 7978, allowing it to be used as a function or structure argument. By ofmresval 7688, 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 7978	Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) ∈ V)
Theorem	mptcnfimad 7979*	The converse of a mapping of subsets to their image of a bijection. (Contributed by AV, 23-Apr-2025.)
⊢ 𝑀 = (𝑥 ∈ 𝐴 ↦ (𝐹 “ 𝑥))    &   ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝒫 𝑉)    &   ⊢ (𝜑 → ran 𝑀 ⊆ 𝒫 𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ◡𝑀 = (𝑦 ∈ ran 𝑀 ↦ (◡𝐹 “ 𝑦)))
2.4.8  First and second members of an ordered pair
Syntax	c1st 7980	Extend the definition of a class to include the first member an ordered pair function.
class 1st
Syntax	c2nd 7981	Extend the definition of a class to include the second member an ordered pair function.
class 2nd
Definition	df-1st 7982	Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 7990 proves that it does this. For example, (1st ‘⟨3, 4⟩) = 3. Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 6223 and op1stb 5451). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
Definition	df-2nd 7983	Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 7991 proves that it does this. For example, (2nd ‘⟨3, 4⟩) = 4. Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 6226 and op2ndb 6225). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥})
Theorem	1stval 7984	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 7985	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 7986	Value of the first-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ (¬ 𝐴 ∈ (V × V) → (1st ‘𝐴) = ∅)
Theorem	2ndnpr 7987	Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ (¬ 𝐴 ∈ (V × V) → (2nd ‘𝐴) = ∅)
Theorem	1st0 7988	The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
⊢ (1st ‘∅) = ∅
Theorem	2nd0 7989	The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
⊢ (2nd ‘∅) = ∅
Theorem	op1st 7990	Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴
Theorem	op2nd 7991	Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
Theorem	op1std 7992	Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1st ‘𝐶) = 𝐴)
Theorem	op2ndd 7993	Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = 𝐵)
Theorem	op1stg 7994	Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)
Theorem	op2ndg 7995	Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)
Theorem	ot1stg 7996	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 7996, ot2ndg 7997, ot3rdg 7998.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (1st ‘(1st ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐴)
Theorem	ot2ndg 7997	Extract the second member of an ordered triple. (See ot1stg 7996 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2nd ‘(1st ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐵)
Theorem	ot3rdg 7998	Extract the third member of an ordered triple. (See ot1stg 7996 comment.) (Contributed by NM, 3-Apr-2015.)
⊢ (𝐶 ∈ 𝑉 → (2nd ‘⟨𝐴, 𝐵, 𝐶⟩) = 𝐶)
Theorem	1stval2 7999	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 8000	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 ‘𝐴) = ∩ ∩ ∩ ◡{𝐴})