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	riotaclb 7401*	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 7402*	Restricted iota of a restricted abstraction. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜓}𝜒) = (℩𝑥 ∈ 𝐴 (𝜑 ∧ 𝜒))
2.3.19  Operations
Syntax	co 7403	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 11465.)
class (𝐴𝐹𝐵)
Syntax	coprab 7404	Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Syntax	cmpo 7405	Extend the definition of a class to include maps-to notation for defining an operation via a rule.
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Definition	df-ov 7406	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 12389). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 7442 and ovprc2 7443. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +o in oav 8521. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 7407. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Definition	df-oprab 7407*	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 7406 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 7565. (Contributed by NM, 12-Mar-1995.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
Definition	df-mpo 7408*	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 5202 for two arguments. (Contributed by NM, 17-Feb-2008.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
Theorem	oveq 7409	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Theorem	oveq1 7410	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
Theorem	oveq2 7411	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Theorem	oveq12 7412	Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveq1i 7413	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)
Theorem	oveq2i 7414	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Theorem	oveq12i 7415	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)
Theorem	oveqi 7416	Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶𝐴𝐷) = (𝐶𝐵𝐷)
Theorem	oveq123i 7417	Equality inference for operation value. (Contributed by FL, 11-Jul-2010.)
⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    &   ⊢ 𝐹 = 𝐺    ⇒   ⊢ (𝐴𝐹𝐵) = (𝐶𝐺𝐷)
Theorem	oveq1d 7418	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
Theorem	oveq2d 7419	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Theorem	oveqd 7420	Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
Theorem	oveq12d 7421	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveqan12d 7422	Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveqan12rd 7423	Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveq123d 7424	Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷))
Theorem	fvoveq1d 7425	Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))
Theorem	fvoveq1 7426	Equality theorem for nested function and operation value. Closed form of fvoveq1d 7425. (Contributed by AV, 23-Jul-2022.)
⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))
Theorem	ovanraleqv 7427*	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 7428	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 7429*	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 7430*	Restricted specialization of operands, using implicit substitution. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐹𝑌) = (𝑋𝐺𝑌))
Theorem	oveqdr 7431	Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
Theorem	nfovd 7432	Deduction version of bound-variable hypothesis builder nfov 7433. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐹)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝐴𝐹𝐵))
Theorem	nfov 7433	Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴𝐹𝐵)
Theorem	oprabidw 7434*	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of oprabid 7435 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by Mario Carneiro, 20-Mar-2013.) Avoid ax-13 2376. (Revised by GG, 26-Jan-2024.)
⊢ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)
Theorem	oprabid 7435	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 2376. Use the weaker oprabidw 7434 when possible. (Contributed by Mario Carneiro, 20-Mar-2013.) (New usage is discouraged.)
⊢ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)
Theorem	ovex 7436	The result of an operation is a set. (Contributed by NM, 13-Mar-1995.)
⊢ (𝐴𝐹𝐵) ∈ V
Theorem	ovexi 7437	The result of an operation is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐴 = (𝐵𝐹𝐶)    ⇒   ⊢ 𝐴 ∈ V
Theorem	ovexd 7438	The result of an operation is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → (𝐴𝐹𝐵) ∈ V)
Theorem	ovssunirn 7439	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 7440	Operation value of the empty set. (Contributed by AV, 15-May-2021.)
⊢ (𝐴∅𝐵) = ∅
Theorem	ovprc 7441	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 7442	The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.)
⊢ Rel dom 𝐹    ⇒   ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅)
Theorem	ovprc2 7443	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 7444	Reverse closure for an operation value. (Contributed by Mario Carneiro, 5-May-2015.)
⊢ Rel dom 𝐹    ⇒   ⊢ (𝐶 ∈ (𝐴𝐹𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	elfvov1 7445	Utility theorem: reverse closure for any operation that results in a function. (Contributed by SN, 18-May-2025.)
⊢ Rel dom 𝑂    &   ⊢ 𝑆 = (𝐼𝑂𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆‘𝑌))    ⇒   ⊢ (𝜑 → 𝐼 ∈ V)
Theorem	elfvov2 7446	Utility theorem: reverse closure for any operation that results in a function. (Contributed by SN, 4-Aug-2025.)
⊢ Rel dom 𝑂    &   ⊢ 𝑆 = (𝐼𝑂𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆‘𝑌))    ⇒   ⊢ (𝜑 → 𝑅 ∈ V)
Theorem	csbov123 7447	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Revised by NM, 23-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝐹⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbov 7448*	Move class substitution in and out of an operation. (Contributed by NM, 23-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (𝐵⦋𝐴 / 𝑥⦌𝐹𝐶)
Theorem	csbov12g 7449*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹⦋𝐴 / 𝑥⦌𝐶))
Theorem	csbov1g 7450*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹𝐶))
Theorem	csbov2g 7451*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (𝐵𝐹⦋𝐴 / 𝑥⦌𝐶))
Theorem	rspceov 7452*	A frequently used special case of rspc2ev 3614 for operation values. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = (𝐶𝐹𝐷)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = (𝑥𝐹𝑦))
Theorem	elovimad 7453	Elementhood of the image set of an operation value. (Contributed by Thierry Arnoux, 13-Mar-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → (𝐶 × 𝐷) ⊆ dom 𝐹)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ (𝐹 “ (𝐶 × 𝐷)))
Theorem	fnbrovb 7454	Value of a binary operation expressed as a binary relation. See also fnbrfvb 6928 for functions on Cartesian products. (Contributed by BJ, 15-Feb-2022.)
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((𝐴𝐹𝐵) = 𝐶 ↔ ⟨𝐴, 𝐵⟩𝐹𝐶))
Theorem	fnotovb 7455	Equivalence of operation value and ordered triple membership, analogous to fnopfvb 6929. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) (Proof shortened by BJ, 15-Feb-2022.)
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ((𝐶𝐹𝐷) = 𝑅 ↔ ⟨𝐶, 𝐷, 𝑅⟩ ∈ 𝐹))
Theorem	opabbrex 7456	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 7457*	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 7458*	Obsolete version of opabresex2 7457 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 7459*	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 7460*	Obsolete version of fvmptopab 7459 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 7461*	Condition for an operation to be one-to-one. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (𝐹:(𝐴 × 𝐵)–1-1→𝐶 ↔ (𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑟 ∈ 𝐴 ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ∀𝑢 ∈ 𝐵 ((𝑟𝐹𝑠) = (𝑡𝐹𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))))
Theorem	brfvopab 7462	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 7463*	Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Theorem	reloprab 7464*	An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.)
⊢ Rel {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	oprabv 7465*	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 7466	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 7467	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 7468	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑧{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	nfoprab 7469*	Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑤𝜑    ⇒   ⊢ Ⅎ𝑤{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	oprabbid 7470*	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 7471*	Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Theorem	oprabbii 7472*	Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
Theorem	ssoprab2 7473	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 5521. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})
Theorem	ssoprab2b 7474	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 5524. Usage of this theorem is discouraged because it depends on ax-13 2376. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) (New usage is discouraged.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓))
Theorem	eqoprab2bw 7475*	Equivalence of ordered pair abstraction subclass and biconditional. Version of eqoprab2b 7476 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by Mario Carneiro, 4-Jan-2017.) Avoid ax-13 2376. (Revised by GG, 26-Jan-2024.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓))
Theorem	eqoprab2b 7476	Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 5527. Usage of this theorem is discouraged because it depends on ax-13 2376. Use the weaker eqoprab2bw 7475 when possible. (Contributed by Mario Carneiro, 4-Jan-2017.) (New usage is discouraged.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓))
Theorem	mpoeq123 7477*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝐴 = 𝐷 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐸 ∧ ∀𝑦 ∈ 𝐵 𝐶 = 𝐹)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpoeq12 7478*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))
Theorem	mpoeq123dva 7479*	An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpoeq123dv 7480*	An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ (𝜑 → 𝐵 = 𝐸)    &   ⊢ (𝜑 → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpoeq123i 7481	An equality inference for the maps-to notation. (Contributed by NM, 15-Jul-2013.)
⊢ 𝐴 = 𝐷    &   ⊢ 𝐵 = 𝐸    &   ⊢ 𝐶 = 𝐹    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)
Theorem	mpoeq3dva 7482*	Slightly more general equality inference for the maps-to notation. (Contributed by NM, 17-Oct-2013.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
Theorem	mpoeq3ia 7483	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	mpoeq3dv 7484*	An equality deduction for the maps-to notation restricted to the value of the operation. (Contributed by SO, 16-Jul-2018.)
⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
Theorem	nfmpo1 7485	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	nfmpo2 7486	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	nfmpo 7487*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    ⇒   ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	0mpo0 7488*	A mapping operation with empty domain is empty. Generalization of mpo0 7490. (Contributed by AV, 27-Jan-2024.)
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅)
Theorem	mpo0v 7489*	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 7490	A mapping operation with empty domain. In this version of mpo0v 7489, 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 7491*	Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)}
Theorem	cbvoprab1 7492*	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 7493*	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 7494*	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 7495*	Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.)
⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑣) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑤, 𝑣⟩, 𝑧⟩ ∣ 𝜓}
Theorem	cbvoprab3 7496*	Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑧𝜓    &   ⊢ (𝑧 = 𝑤 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ 𝜓}
Theorem	cbvoprab3v 7497*	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.)
⊢ (𝑧 = 𝑤 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ 𝜓}
Theorem	cbvmpox 7498*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo 7499 allows 𝐵 to be a function of 𝑥. (Contributed by NM, 29-Dec-2014.)
⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑤𝐶    &   ⊢ Ⅎ𝑥𝐸    &   ⊢ Ⅎ𝑦𝐸    &   ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐷)    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐸)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐷 ↦ 𝐸)
Theorem	cbvmpo 7499*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.)
⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑤𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ Ⅎ𝑦𝐷    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)
Theorem	cbvmpov 7500*	Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 5223, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)
⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)    &   ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)