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	ovex 7401	The result of an operation is a set. (Contributed by NM, 13-Mar-1995.)
⊢ (𝐴𝐹𝐵) ∈ V
Theorem	ovexi 7402	The result of an operation is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐴 = (𝐵𝐹𝐶)    ⇒   ⊢ 𝐴 ∈ V
Theorem	ovexd 7403	The result of an operation is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → (𝐴𝐹𝐵) ∈ V)
Theorem	ovssunirn 7404	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 7405	Operation value of the empty set. (Contributed by AV, 15-May-2021.)
⊢ (𝐴∅𝐵) = ∅
Theorem	ovprc 7406	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 7407	The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.)
⊢ Rel dom 𝐹    ⇒   ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅)
Theorem	ovprc2 7408	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 7409	Reverse closure for an operation value. (Contributed by Mario Carneiro, 5-May-2015.)
⊢ Rel dom 𝐹    ⇒   ⊢ (𝐶 ∈ (𝐴𝐹𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	elfvov1 7410	Utility theorem: reverse closure for any operation that results in a function. (Contributed by SN, 18-May-2025.)
⊢ Rel dom 𝑂    &   ⊢ 𝑆 = (𝐼𝑂𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆‘𝑌))    ⇒   ⊢ (𝜑 → 𝐼 ∈ V)
Theorem	elfvov2 7411	Utility theorem: reverse closure for any operation that results in a function. (Contributed by SN, 4-Aug-2025.)
⊢ Rel dom 𝑂    &   ⊢ 𝑆 = (𝐼𝑂𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆‘𝑌))    ⇒   ⊢ (𝜑 → 𝑅 ∈ V)
Theorem	csbov123 7412	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Revised by NM, 23-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝐹⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbov 7413*	Move class substitution in and out of an operation. (Contributed by NM, 23-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (𝐵⦋𝐴 / 𝑥⦌𝐹𝐶)
Theorem	csbov12g 7414*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹⦋𝐴 / 𝑥⦌𝐶))
Theorem	csbov1g 7415*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹𝐶))
Theorem	csbov2g 7416*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (𝐵𝐹⦋𝐴 / 𝑥⦌𝐶))
Theorem	rspceov 7417*	A frequently used special case of rspc2ev 3591 for operation values. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = (𝐶𝐹𝐷)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = (𝑥𝐹𝑦))
Theorem	elovimad 7418	Elementhood of the image set of an operation value. (Contributed by Thierry Arnoux, 13-Mar-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → (𝐶 × 𝐷) ⊆ dom 𝐹)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ (𝐹 “ (𝐶 × 𝐷)))
Theorem	fnbrovb 7419	Value of a binary operation expressed as a binary relation. See also fnbrfvb 6892 for functions on Cartesian products. (Contributed by BJ, 15-Feb-2022.)
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((𝐴𝐹𝐵) = 𝐶 ↔ ⟨𝐴, 𝐵⟩𝐹𝐶))
Theorem	fnotovb 7420	Equivalence of operation value and ordered triple membership, analogous to fnopfvb 6893. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) (Proof shortened by BJ, 15-Feb-2022.)
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ((𝐶𝐹𝐷) = 𝑅 ↔ ⟨𝐶, 𝐷, 𝑅⟩ ∈ 𝐹))
Theorem	opabbrex 7421	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 7422*	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	fvmptopab 7423*	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	f1opr 7424*	Condition for an operation to be one-to-one. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (𝐹:(𝐴 × 𝐵)–1-1→𝐶 ↔ (𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑟 ∈ 𝐴 ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ∀𝑢 ∈ 𝐵 ((𝑟𝐹𝑠) = (𝑡𝐹𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))))
Theorem	brfvopab 7425	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 7426*	Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Theorem	reloprab 7427*	An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.)
⊢ Rel {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	oprabv 7428*	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 7429	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 7430	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 7431	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑧{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	nfoprab 7432*	Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑤𝜑    ⇒   ⊢ Ⅎ𝑤{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	oprabbid 7433*	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 7434*	Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Theorem	oprabbii 7435*	Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
Theorem	ssoprab2 7436	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 5502. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})
Theorem	ssoprab2b 7437	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 5505. Usage of this theorem is discouraged because it depends on ax-13 2377. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) (New usage is discouraged.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓))
Theorem	eqoprab2bw 7438*	Equivalence of ordered pair abstraction subclass and biconditional. Version of eqoprab2b 7439 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by Mario Carneiro, 4-Jan-2017.) Avoid ax-13 2377. (Revised by GG, 26-Jan-2024.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓))
Theorem	eqoprab2b 7439	Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 5508. Usage of this theorem is discouraged because it depends on ax-13 2377. Use the weaker eqoprab2bw 7438 when possible. (Contributed by Mario Carneiro, 4-Jan-2017.) (New usage is discouraged.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓))
Theorem	mpoeq123 7440*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝐴 = 𝐷 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐸 ∧ ∀𝑦 ∈ 𝐵 𝐶 = 𝐹)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpoeq12 7441*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))
Theorem	mpoeq123dva 7442*	An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpoeq123dv 7443*	An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ (𝜑 → 𝐵 = 𝐸)    &   ⊢ (𝜑 → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpoeq123i 7444	An equality inference for the maps-to notation. (Contributed by NM, 15-Jul-2013.)
⊢ 𝐴 = 𝐷    &   ⊢ 𝐵 = 𝐸    &   ⊢ 𝐶 = 𝐹    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)
Theorem	mpoeq3dva 7445*	Slightly more general equality inference for the maps-to notation. (Contributed by NM, 17-Oct-2013.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
Theorem	mpoeq3ia 7446	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	mpoeq3dv 7447*	An equality deduction for the maps-to notation restricted to the value of the operation. (Contributed by SO, 16-Jul-2018.)
⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
Theorem	nfmpo1 7448	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	nfmpo2 7449	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	nfmpo 7450*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    ⇒   ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	0mpo0 7451*	A mapping operation with empty domain is empty. Generalization of mpo0 7453. (Contributed by AV, 27-Jan-2024.)
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅)
Theorem	mpo0v 7452*	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 7453	A mapping operation with empty domain. In this version of mpo0v 7452, 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 7454*	Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)}
Theorem	cbvoprab1 7455*	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 7456*	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 7457*	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 7458*	Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.)
⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑣) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑤, 𝑣⟩, 𝑧⟩ ∣ 𝜓}
Theorem	cbvoprab3 7459*	Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑧𝜓    &   ⊢ (𝑧 = 𝑤 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ 𝜓}
Theorem	cbvoprab3v 7460*	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 7461*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo 7462 allows 𝐵 to be a function of 𝑥. (Contributed by NM, 29-Dec-2014.)
⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑤𝐶    &   ⊢ Ⅎ𝑥𝐸    &   ⊢ Ⅎ𝑦𝐸    &   ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐷)    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐸)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐷 ↦ 𝐸)
Theorem	cbvmpo 7462*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.)
⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑤𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ Ⅎ𝑦𝐷    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)
Theorem	cbvmpov 7463*	Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 5202, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)
⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)    &   ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)
Theorem	elimdelov 7464	Eliminate a hypothesis which is a predicate expressing membership in the result of an operator (deduction version). (Contributed by Paul Chapman, 25-Mar-2008.)
⊢ (𝜑 → 𝐶 ∈ (𝐴𝐹𝐵))    &   ⊢ 𝑍 ∈ (𝑋𝐹𝑌)    ⇒   ⊢ if(𝜑, 𝐶, 𝑍) ∈ (if(𝜑, 𝐴, 𝑋)𝐹if(𝜑, 𝐵, 𝑌))
Theorem	brif1 7465	Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024.)
⊢ (if(𝜑, 𝐴, 𝐵)𝑅𝐶 ↔ if-(𝜑, 𝐴𝑅𝐶, 𝐵𝑅𝐶))
Theorem	ovif 7466	Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (if(𝜑, 𝐴, 𝐵)𝐹𝐶) = if(𝜑, (𝐴𝐹𝐶), (𝐵𝐹𝐶))
Theorem	ovif2 7467	Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 1-Oct-2018.)
⊢ (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = if(𝜑, (𝐴𝐹𝐵), (𝐴𝐹𝐶))
Theorem	ovif12 7468	Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (if(𝜑, 𝐴, 𝐵)𝐹if(𝜑, 𝐶, 𝐷)) = if(𝜑, (𝐴𝐹𝐶), (𝐵𝐹𝐷))
Theorem	ifov 7469	Move a conditional outside of an operation. (Contributed by AV, 11-Nov-2019.)
⊢ (𝐴if(𝜑, 𝐹, 𝐺)𝐵) = if(𝜑, (𝐴𝐹𝐵), (𝐴𝐺𝐵))
Theorem	ifmpt2v 7470*	Move a conditional inside and outside a function in maps-to notation. (Contributed by SN, 16-Oct-2025.)
⊢ (𝑥 ∈ 𝐴 ↦ if(𝜑, 𝐵, 𝐶)) = if(𝜑, (𝑥 ∈ 𝐴 ↦ 𝐵), (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	dmoprab 7471*	The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝜑}
Theorem	dmoprabss 7472*	The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995.)
⊢ dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)
Theorem	rnoprab 7473*	The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)
⊢ ran {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦𝜑}
Theorem	rnoprab2 7474*	The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.)
⊢ ran {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑}
Theorem	reldmoprab 7475*	The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)
⊢ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	oprabss 7476*	Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ ((V × V) × V)
Theorem	eloprabga 7477*	The law of concretion for operation class abstraction. Compare elopab 5483. (Contributed by NM, 14-Sep-1999.) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.) Avoid ax-10 2147, ax-11 2163. (Revised by Wolf Lammen, 15-Oct-2024.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜓))
Theorem	eloprabg 7478*	The law of concretion for operation class abstraction. Compare elopab 5483. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜃))
Theorem	ssoprab2i 7479*	Inference of operation class abstraction subclass from implication. (Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
Theorem	mpov 7480*	Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑧 = 𝐶}
Theorem	mpomptx 7481*	Express a two-argument function as a one-argument function, or vice-versa. In this version 𝐵(𝑥) is not assumed to be constant w.r.t 𝑥. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	mpompt 7482*	Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by Mario Carneiro, 29-Dec-2014.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	mpodifsnif 7483	A mapping with two arguments with the first argument from a difference set with a singleton and a conditional as result. (Contributed by AV, 13-Feb-2019.)
⊢ (𝑖 ∈ (𝐴 ∖ {𝑋}), 𝑗 ∈ 𝐵 ↦ if(𝑖 = 𝑋, 𝐶, 𝐷)) = (𝑖 ∈ (𝐴 ∖ {𝑋}), 𝑗 ∈ 𝐵 ↦ 𝐷)
Theorem	mposnif 7484	A mapping with two arguments with the first argument from a singleton and a conditional as result. (Contributed by AV, 14-Feb-2019.)
⊢ (𝑖 ∈ {𝑋}, 𝑗 ∈ 𝐵 ↦ if(𝑖 = 𝑋, 𝐶, 𝐷)) = (𝑖 ∈ {𝑋}, 𝑗 ∈ 𝐵 ↦ 𝐶)
Theorem	fconstmpo 7485*	Representation of a constant operation using the mapping operation. (Contributed by SO, 11-Jul-2018.)
⊢ ((𝐴 × 𝐵) × {𝐶}) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	resoprab 7486*	Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↾ (𝐴 × 𝐵)) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)}
Theorem	resoprab2 7487*	Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ↾ (𝐶 × 𝐷)) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)})
Theorem	resmpo 7488*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) ↾ (𝐶 × 𝐷)) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))
Theorem	funoprabg 7489*	"At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 28-Aug-2007.)
⊢ (∀𝑥∀𝑦∃*𝑧𝜑 → Fun {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑})
Theorem	funoprab 7490*	"At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 17-Mar-1995.)
⊢ ∃*𝑧𝜑    ⇒   ⊢ Fun {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	fnoprabg 7491*	Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007.)
⊢ (∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (𝜑 ∧ 𝜓)} Fn {⟨𝑥, 𝑦⟩ ∣ 𝜑})
Theorem	mpofun 7492*	The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.) (Proof shortened by SN, 23-Jul-2024.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ Fun 𝐹
Theorem	fnoprab 7493*	Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995.)
⊢ (𝜑 → ∃!𝑧𝜓)    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (𝜑 ∧ 𝜓)} Fn {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	ffnov 7494*	An operation maps to a class to which all values belong. (Contributed by NM, 7-Feb-2004.)
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶))
Theorem	fovcld 7495	Closure law for an operation. (Contributed by NM, 19-Apr-2007.) (Revised by Thierry Arnoux, 17-Feb-2017.)
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
Theorem	fovcl 7496	Closure law for an operation. (Contributed by NM, 19-Apr-2007.) (Proof shortened by AV, 9-Mar-2025.)
⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
Theorem	eqfnov 7497*	Equality of two operations is determined by their values. (Contributed by NM, 1-Sep-2005.)
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐶 × 𝐷)) → (𝐹 = 𝐺 ↔ ((𝐴 × 𝐵) = (𝐶 × 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦))))
Theorem	eqfnov2 7498*	Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010.)
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐴 × 𝐵)) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦)))
Theorem	fnov 7499*	Representation of a function in terms of its values. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐹 Fn (𝐴 × 𝐵) ↔ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝑥𝐹𝑦)))
Theorem	mpo2eqb 7500*	Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 7498. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 = 𝐷))