P. 75 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7401-7500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eusvobj1 7401*	Specify the same object in two ways when class 𝐵(𝑦) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 → (℩𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵) = (℩𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))
Theorem	f1ofveu 7402*	There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃!𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐶)
Theorem	f1ocnvfv3 7403*	Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) = (℩𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐶))
Theorem	riotaund 7404*	Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 13-Sep-2018.)
⊢ (¬ ∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) = ∅)
Theorem	riotassuni 7405*	The restricted iota class is limited in size by the base set. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (℩𝑥 ∈ 𝐴 𝜑) ⊆ (𝒫 ∪ 𝐴 ∪ ∪ 𝐴)
Theorem	riotaclb 7406*	Bidirectional closure of restricted iota when domain is not empty. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.) (Revised by NM, 13-Sep-2018.)
⊢ (¬ ∅ ∈ 𝐴 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴))
Theorem	riotarab 7407*	Restricted iota of a restricted abstraction. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜓}𝜒) = (℩𝑥 ∈ 𝐴 (𝜑 ∧ 𝜒))
2.3.19  Operations
Syntax	co 7408	Extend class notation to include the value of an operation 𝐹 (such as +) for two arguments 𝐴 and 𝐵. Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous. (For an example of how syntax could become ambiguous if we are not careful, see the comment in cneg 11444.)
class (𝐴𝐹𝐵)
Syntax	coprab 7409	Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Syntax	cmpo 7410	Extend the definition of a class to include maps-to notation for defining an operation via a rule.
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Definition	df-ov 7411	Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. For example, if class 𝐹 is the operation + and arguments 𝐴 and 𝐵 are 3 and 2, the expression (3 + 2) can be proved to equal 5 (see 3p2e5 12362). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 7447 and ovprc2 7448. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +o in oav 8510. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 7412. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Definition	df-oprab 7412*	Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally 𝑥, 𝑦, and 𝑧 are distinct, although the definition doesn't strictly require it. See df-ov 7411 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of an operation given by a class abstraction is given by ovmpo 7567. (Contributed by NM, 12-Mar-1995.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
Definition	df-mpo 7413*	Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from 𝑥, 𝑦 (in 𝐴 × 𝐵) to 𝐶(𝑥, 𝑦)". An extension of df-mpt 5232 for two arguments. (Contributed by NM, 17-Feb-2008.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
Theorem	oveq 7414	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Theorem	oveq1 7415	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
Theorem	oveq2 7416	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Theorem	oveq12 7417	Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveq1i 7418	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)
Theorem	oveq2i 7419	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Theorem	oveq12i 7420	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)
Theorem	oveqi 7421	Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶𝐴𝐷) = (𝐶𝐵𝐷)
Theorem	oveq123i 7422	Equality inference for operation value. (Contributed by FL, 11-Jul-2010.)
⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    &   ⊢ 𝐹 = 𝐺    ⇒   ⊢ (𝐴𝐹𝐵) = (𝐶𝐺𝐷)
Theorem	oveq1d 7423	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
Theorem	oveq2d 7424	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Theorem	oveqd 7425	Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
Theorem	oveq12d 7426	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveqan12d 7427	Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveqan12rd 7428	Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveq123d 7429	Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷))
Theorem	fvoveq1d 7430	Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))
Theorem	fvoveq1 7431	Equality theorem for nested function and operation value. Closed form of fvoveq1d 7430. (Contributed by AV, 23-Jul-2022.)
⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))
Theorem	ovanraleqv 7432*	Equality theorem for a conjunction with an operation values within a restricted universal quantification. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.)
⊢ (𝐵 = 𝑋 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 = 𝑋 → (∀𝑥 ∈ 𝑉 (𝜑 ∧ (𝐴 · 𝐵) = 𝐶) ↔ ∀𝑥 ∈ 𝑉 (𝜓 ∧ (𝐴 · 𝑋) = 𝐶)))
Theorem	imbrov2fvoveq 7433	Equality theorem for nested function and operation value in an implication for a binary relation. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 17-Aug-2022.)
⊢ (𝑋 = 𝑌 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑋 = 𝑌 → ((𝜑 → (𝐹‘((𝐺‘𝑋) · 𝑂))𝑅𝐴) ↔ (𝜓 → (𝐹‘((𝐺‘𝑌) · 𝑂))𝑅𝐴)))
Theorem	ovrspc2v 7434*	If an operation value is element of a class for all operands of two classes, then the operation value is an element of the class for specific operands of the two classes. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶) → (𝑋𝐹𝑌) ∈ 𝐶)
Theorem	oveqrspc2v 7435*	Restricted specialization of operands, using implicit substitution. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐹𝑌) = (𝑋𝐺𝑌))
Theorem	oveqdr 7436	Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
Theorem	nfovd 7437	Deduction version of bound-variable hypothesis builder nfov 7438. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐹)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝐴𝐹𝐵))
Theorem	nfov 7438	Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴𝐹𝐵)
Theorem	oprabidw 7439*	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of oprabid 7440 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Mario Carneiro, 20-Mar-2013.) Avoid ax-13 2371. (Revised by Gino Giotto, 26-Jan-2024.)
⊢ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)
Theorem	oprabid 7440	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker oprabidw 7439 when possible. (Contributed by Mario Carneiro, 20-Mar-2013.) (New usage is discouraged.)
⊢ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)
Theorem	ovex 7441	The result of an operation is a set. (Contributed by NM, 13-Mar-1995.)
⊢ (𝐴𝐹𝐵) ∈ V
Theorem	ovexi 7442	The result of an operation is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐴 = (𝐵𝐹𝐶)    ⇒   ⊢ 𝐴 ∈ V
Theorem	ovexd 7443	The result of an operation is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → (𝐴𝐹𝐵) ∈ V)
Theorem	ovssunirn 7444	The result of an operation value is always a subset of the union of the range. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝑋𝐹𝑌) ⊆ ∪ ran 𝐹
Theorem	0ov 7445	Operation value of the empty set. (Contributed by AV, 15-May-2021.)
⊢ (𝐴∅𝐵) = ∅
Theorem	ovprc 7446	The value of an operation when the one of the arguments is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ Rel dom 𝐹    ⇒   ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅)
Theorem	ovprc1 7447	The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.)
⊢ Rel dom 𝐹    ⇒   ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅)
Theorem	ovprc2 7448	The value of an operation when the second argument is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ Rel dom 𝐹    ⇒   ⊢ (¬ 𝐵 ∈ V → (𝐴𝐹𝐵) = ∅)
Theorem	ovrcl 7449	Reverse closure for an operation value. (Contributed by Mario Carneiro, 5-May-2015.)
⊢ Rel dom 𝐹    ⇒   ⊢ (𝐶 ∈ (𝐴𝐹𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	csbov123 7450	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Revised by NM, 23-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝐹⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbov 7451*	Move class substitution in and out of an operation. (Contributed by NM, 23-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (𝐵⦋𝐴 / 𝑥⦌𝐹𝐶)
Theorem	csbov12g 7452*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹⦋𝐴 / 𝑥⦌𝐶))
Theorem	csbov1g 7453*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹𝐶))
Theorem	csbov2g 7454*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (𝐵𝐹⦋𝐴 / 𝑥⦌𝐶))
Theorem	rspceov 7455*	A frequently used special case of rspc2ev 3624 for operation values. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = (𝐶𝐹𝐷)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = (𝑥𝐹𝑦))
Theorem	elovimad 7456	Elementhood of the image set of an operation value. (Contributed by Thierry Arnoux, 13-Mar-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → (𝐶 × 𝐷) ⊆ dom 𝐹)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ (𝐹 “ (𝐶 × 𝐷)))
Theorem	fnbrovb 7457	Value of a binary operation expressed as a binary relation. See also fnbrfvb 6944 for functions on Cartesian products. (Contributed by BJ, 15-Feb-2022.)
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((𝐴𝐹𝐵) = 𝐶 ↔ ⟨𝐴, 𝐵⟩𝐹𝐶))
Theorem	fnotovb 7458	Equivalence of operation value and ordered triple membership, analogous to fnopfvb 6945. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) (Proof shortened by BJ, 15-Feb-2022.)
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ((𝐶𝐹𝐷) = 𝑅 ↔ ⟨𝐶, 𝐷, 𝑅⟩ ∈ 𝐹))
Theorem	opabbrex 7459	A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by BJ/AV, 20-Jun-2019.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ ((∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝜑) ∧ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∈ 𝑉) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑅𝑦 ∧ 𝜓)} ∈ V)
Theorem	opabresex2 7460*	Restrictions of a collection of ordered pairs of related elements are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 15-Jan-2021.) Add disjoint variable conditions betweem 𝑊, 𝐺 and 𝑥, 𝑦 to remove hypotheses. (Revised by SN, 13-Dec-2024.)
⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥(𝑊‘𝐺)𝑦 ∧ 𝜃)} ∈ V
Theorem	opabresex2d 7461*	Obsolete version of opabresex2 7460 as of 13-Dec-2024. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 15-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥(𝑊‘𝐺)𝑦) → 𝜓)    &   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} ∈ 𝑉)    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥(𝑊‘𝐺)𝑦 ∧ 𝜃)} ∈ V)
Theorem	fvmptopab 7462*	The function value of a mapping 𝑀 to a restricted binary relation expressed as an ordered-pair class abstraction: The restricted binary relation is a binary relation given as value of a function 𝐹 restricted by the condition 𝜓. (Contributed by AV, 31-Jan-2021.) (Revised by AV, 29-Oct-2021.) Add disjoint variable condition on 𝐹, 𝑥, 𝑦 to remove a sethood hypothesis. (Revised by SN, 13-Dec-2024.)
⊢ (𝑧 = 𝑍 → (𝜑 ↔ 𝜓))    &   ⊢ 𝑀 = (𝑧 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥(𝐹‘𝑧)𝑦 ∧ 𝜑)})    ⇒   ⊢ (𝑀‘𝑍) = {⟨𝑥, 𝑦⟩ ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)}
Theorem	fvmptopabOLD 7463*	Obsolete version of fvmptopab 7462 as of 13-Dec-2024. (Contributed by AV, 31-Jan-2021.) (Revised by AV, 29-Oct-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑧 = 𝑍) → (𝜒 ↔ 𝜓))    &   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝑥(𝐹‘𝑍)𝑦} ∈ V)    &   ⊢ 𝑀 = (𝑧 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥(𝐹‘𝑧)𝑦 ∧ 𝜒)})    ⇒   ⊢ (𝜑 → (𝑀‘𝑍) = {⟨𝑥, 𝑦⟩ ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)})
Theorem	f1opr 7464*	Condition for an operation to be one-to-one. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (𝐹:(𝐴 × 𝐵)–1-1→𝐶 ↔ (𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑟 ∈ 𝐴 ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ∀𝑢 ∈ 𝐵 ((𝑟𝐹𝑠) = (𝑡𝐹𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))))
Theorem	brfvopab 7465	The classes involved in a binary relation of a function value which is an ordered-pair class abstraction are sets. (Contributed by AV, 7-Jan-2021.)
⊢ (𝑋 ∈ V → (𝐹‘𝑋) = {⟨𝑦, 𝑧⟩ ∣ 𝜑})    ⇒   ⊢ (𝐴(𝐹‘𝑋)𝐵 → (𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	dfoprab2 7466*	Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Theorem	reloprab 7467*	An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.)
⊢ Rel {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	oprabv 7468*	If a pair and a class are in a relationship given by a class abstraction of a collection of nested ordered pairs, the involved classes are sets. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
⊢ (⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍 → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V))
Theorem	nfoprab1 7469	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ Ⅎ𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	nfoprab2 7470	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 30-Jul-2012.)
⊢ Ⅎ𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	nfoprab3 7471	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑧{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	nfoprab 7472*	Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑤𝜑    ⇒   ⊢ Ⅎ𝑤{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	oprabbid 7473*	Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Theorem	oprabbidv 7474*	Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Theorem	oprabbii 7475*	Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
Theorem	ssoprab2 7476	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 5546. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})
Theorem	ssoprab2b 7477	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 5549. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) (New usage is discouraged.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓))
Theorem	eqoprab2bw 7478*	Equivalence of ordered pair abstraction subclass and biconditional. Version of eqoprab2b 7479 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Mario Carneiro, 4-Jan-2017.) Avoid ax-13 2371. (Revised by Gino Giotto, 26-Jan-2024.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓))
Theorem	eqoprab2b 7479	Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 5552. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker eqoprab2bw 7478 when possible. (Contributed by Mario Carneiro, 4-Jan-2017.) (New usage is discouraged.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓))
Theorem	mpoeq123 7480*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝐴 = 𝐷 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐸 ∧ ∀𝑦 ∈ 𝐵 𝐶 = 𝐹)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpoeq12 7481*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))
Theorem	mpoeq123dva 7482*	An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpoeq123dv 7483*	An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ (𝜑 → 𝐵 = 𝐸)    &   ⊢ (𝜑 → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpoeq123i 7484	An equality inference for the maps-to notation. (Contributed by NM, 15-Jul-2013.)
⊢ 𝐴 = 𝐷    &   ⊢ 𝐵 = 𝐸    &   ⊢ 𝐶 = 𝐹    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)
Theorem	mpoeq3dva 7485*	Slightly more general equality inference for the maps-to notation. (Contributed by NM, 17-Oct-2013.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
Theorem	mpoeq3ia 7486	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	mpoeq3dv 7487*	An equality deduction for the maps-to notation restricted to the value of the operation. (Contributed by SO, 16-Jul-2018.)
⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
Theorem	nfmpo1 7488	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	nfmpo2 7489	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	nfmpo 7490*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    ⇒   ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	0mpo0 7491*	A mapping operation with empty domain is empty. Generalization of mpo0 7493. (Contributed by AV, 27-Jan-2024.)
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅)
Theorem	mpo0v 7492*	A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.) (Proof shortened by AV, 27-Jan-2024.)
⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅
Theorem	mpo0 7493	A mapping operation with empty domain. In this version of mpo0v 7492, the class of the second operator may depend on the first operator. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅
Theorem	oprab4 7494*	Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)}
Theorem	cbvoprab1 7495*	Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008.) (Revised by Mario Carneiro, 5-Dec-2016.)
⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑤, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
Theorem	cbvoprab2 7496*	Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑤 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑤⟩, 𝑧⟩ ∣ 𝜓}
Theorem	cbvoprab12 7497*	Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑣𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑣) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑤, 𝑣⟩, 𝑧⟩ ∣ 𝜓}
Theorem	cbvoprab12v 7498*	Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.)
⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑣) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑤, 𝑣⟩, 𝑧⟩ ∣ 𝜓}
Theorem	cbvoprab3 7499*	Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑧𝜓    &   ⊢ (𝑧 = 𝑤 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ 𝜓}
Theorem	cbvoprab3v 7500*	Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝑧 = 𝑤 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ 𝜓}