P. 58 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5701-5800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oveq2i 5701	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Theorem	oveq12i 5702	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)
Theorem	oveqi 5703	Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶𝐴𝐷) = (𝐶𝐵𝐷)
Theorem	oveq123i 5704	Equality inference for operation value. (Contributed by FL, 11-Jul-2010.)
⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    &   ⊢ 𝐹 = 𝐺    ⇒   ⊢ (𝐴𝐹𝐵) = (𝐶𝐺𝐷)
Theorem	oveq1d 5705	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
Theorem	oveq2d 5706	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Theorem	oveqd 5707	Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
Theorem	oveq12d 5708	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveqan12d 5709	Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveqan12rd 5710	Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveq123d 5711	Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷))
Theorem	fvoveq1d 5712	Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))
Theorem	fvoveq1 5713	Equality theorem for nested function and operation value. Closed form of fvoveq1d 5712. (Contributed by AV, 23-Jul-2022.)
⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))
Theorem	ovanraleqv 5714*	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 5715	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	nfovd 5716	Deduction version of bound-variable hypothesis builder nfov 5717. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐹)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝐴𝐹𝐵))
Theorem	nfov 5717	Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴𝐹𝐵)
Theorem	oprabidlem 5718*	Slight elaboration of exdistrfor 1735. A lemma for oprabid 5719. (Contributed by Jim Kingdon, 15-Jan-2019.)
⊢ (∃𝑥∃𝑦(𝑥 = 𝑧 ∧ 𝜓) → ∃𝑥(𝑥 = 𝑧 ∧ ∃𝑦𝜓))
Theorem	oprabid 5719	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Although this theorem would be useful with a distinct variable constraint between 𝑥, 𝑦, and 𝑧, we use ax-bndl 1451 to eliminate that constraint. (Contributed by Mario Carneiro, 20-Mar-2013.)
⊢ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)
Theorem	fnovex 5720	The result of an operation is a set. (Contributed by Jim Kingdon, 15-Jan-2019.)
⊢ ((𝐹 Fn (𝐶 × 𝐷) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) ∈ V)
Theorem	ovexg 5721	Evaluating a set operation at two sets gives a set. (Contributed by Jim Kingdon, 19-Aug-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐹𝐵) ∈ V)
Theorem	ovprc 5722	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 5723	The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.)
⊢ Rel dom 𝐹    ⇒   ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅)
Theorem	ovprc2 5724	The value of an operation when the second argument is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ Rel dom 𝐹    ⇒   ⊢ (¬ 𝐵 ∈ V → (𝐴𝐹𝐵) = ∅)
Theorem	csbov123g 5725	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝐹⦋𝐴 / 𝑥⦌𝐶))
Theorem	csbov12g 5726*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹⦋𝐴 / 𝑥⦌𝐶))
Theorem	csbov1g 5727*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹𝐶))
Theorem	csbov2g 5728*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (𝐵𝐹⦋𝐴 / 𝑥⦌𝐶))
Theorem	rspceov 5729*	A frequently used special case of rspc2ev 2750 for operation values. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = (𝐶𝐹𝐷)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = (𝑥𝐹𝑦))
Theorem	fnotovb 5730	Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5381. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ((𝐶𝐹𝐷) = 𝑅 ↔ ⟨𝐶, 𝐷, 𝑅⟩ ∈ 𝐹))
Theorem	opabbrex 5731*	A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑓(𝑉𝑊𝐸)𝑝 → 𝜃))    &   ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → {⟨𝑓, 𝑝⟩ ∣ 𝜃} ∈ V)    ⇒   ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑉𝑊𝐸)𝑝 ∧ 𝜓)} ∈ V)
Theorem	0neqopab 5732	The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.)
⊢ ¬ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	brabvv 5733*	If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Jim Kingdon, 16-Jan-2019.)
⊢ (𝑋{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑌 → (𝑋 ∈ V ∧ 𝑌 ∈ V))
Theorem	dfoprab2 5734*	Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Theorem	reloprab 5735*	An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.)
⊢ Rel {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	nfoprab1 5736	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 5737	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 5738	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑧{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	nfoprab 5739*	Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑤𝜑    ⇒   ⊢ Ⅎ𝑤{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	oprabbid 5740*	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 5741*	Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Theorem	oprabbii 5742*	Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
Theorem	ssoprab2 5743	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 4126. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})
Theorem	ssoprab2b 5744	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 4127. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓))
Theorem	eqoprab2b 5745	Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 4130. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓))
Theorem	mpt2eq123 5746*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝐴 = 𝐷 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐸 ∧ ∀𝑦 ∈ 𝐵 𝐶 = 𝐹)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpt2eq12 5747*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))
Theorem	mpt2eq123dva 5748*	An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpt2eq123dv 5749*	An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ (𝜑 → 𝐵 = 𝐸)    &   ⊢ (𝜑 → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpt2eq123i 5750	An equality inference for the maps-to notation. (Contributed by NM, 15-Jul-2013.)
⊢ 𝐴 = 𝐷    &   ⊢ 𝐵 = 𝐸    &   ⊢ 𝐶 = 𝐹    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)
Theorem	mpt2eq3dva 5751*	Slightly more general equality inference for the maps-to notation. (Contributed by NM, 17-Oct-2013.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
Theorem	mpt2eq3ia 5752	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	nfmpt21 5753	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	nfmpt22 5754	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	nfmpt2 5755*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    ⇒   ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	mpt20 5756	A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅
Theorem	oprab4 5757*	Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)}
Theorem	cbvoprab1 5758*	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 5759*	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 5760*	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 5761*	Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.)
⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑣) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑤, 𝑣⟩, 𝑧⟩ ∣ 𝜓}
Theorem	cbvoprab3 5762*	Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑧𝜓    &   ⊢ (𝑧 = 𝑤 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ 𝜓}
Theorem	cbvoprab3v 5763*	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	cbvmpt2x 5764*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 5765 allows 𝐵 to be a function of 𝑥. (Contributed by NM, 29-Dec-2014.)
⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑤𝐶    &   ⊢ Ⅎ𝑥𝐸    &   ⊢ Ⅎ𝑦𝐸    &   ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐷)    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐸)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐷 ↦ 𝐸)
Theorem	cbvmpt2 5765*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.)
⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑤𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ Ⅎ𝑦𝐷    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)
Theorem	cbvmpt2v 5766*	Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 3955, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)
⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)    &   ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)
Theorem	dmoprab 5767*	The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝜑}
Theorem	dmoprabss 5768*	The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995.)
⊢ dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)
Theorem	rnoprab 5769*	The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)
⊢ ran {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦𝜑}
Theorem	rnoprab2 5770*	The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.)
⊢ ran {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑}
Theorem	reldmoprab 5771*	The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)
⊢ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	oprabss 5772*	Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ ((V × V) × V)
Theorem	eloprabga 5773*	The law of concretion for operation class abstraction. Compare elopab 4109. (Contributed by NM, 14-Sep-1999.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜓))
Theorem	eloprabg 5774*	The law of concretion for operation class abstraction. Compare elopab 4109. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜃))
Theorem	ssoprab2i 5775*	Inference of operation class abstraction subclass from implication. (Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
Theorem	mpt2v 5776*	Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑧 = 𝐶}
Theorem	mpt2mptx 5777*	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	mpt2mpt 5778*	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	resoprab 5779*	Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↾ (𝐴 × 𝐵)) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)}
Theorem	resoprab2 5780*	Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ↾ (𝐶 × 𝐷)) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)})
Theorem	resmpt2 5781*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) ↾ (𝐶 × 𝐷)) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))
Theorem	funoprabg 5782*	"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 5783*	"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 5784*	Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007.)
⊢ (∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (𝜑 ∧ 𝜓)} Fn {⟨𝑥, 𝑦⟩ ∣ 𝜑})
Theorem	mpt2fun 5785*	The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ Fun 𝐹
Theorem	fnoprab 5786*	Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995.)
⊢ (𝜑 → ∃!𝑧𝜓)    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (𝜑 ∧ 𝜓)} Fn {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	ffnov 5787*	An operation maps to a class to which all values belong. (Contributed by NM, 7-Feb-2004.)
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶))
Theorem	fovcl 5788	Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
Theorem	eqfnov 5789*	Equality of two operations is determined by their values. (Contributed by NM, 1-Sep-2005.)
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐶 × 𝐷)) → (𝐹 = 𝐺 ↔ ((𝐴 × 𝐵) = (𝐶 × 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦))))
Theorem	eqfnov2 5790*	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	fnovim 5791*	Representation of a function in terms of its values. (Contributed by Jim Kingdon, 16-Jan-2019.)
⊢ (𝐹 Fn (𝐴 × 𝐵) → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝑥𝐹𝑦)))
Theorem	mpt22eqb 5792*	Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 5790. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 = 𝐷))
Theorem	rnmpt2 5793*	The range of an operation given by the maps-to notation. (Contributed by FL, 20-Jun-2011.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶}
Theorem	reldmmpt2 5794*	The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ Rel dom 𝐹
Theorem	elrnmpt2g 5795*	Membership in the range of an operation class abstraction. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (𝐷 ∈ 𝑉 → (𝐷 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶))
Theorem	elrnmpt2 5796*	Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐷 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶)
Theorem	ralrnmpt2 5797*	A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ (𝑧 = 𝐶 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → (∀𝑧 ∈ ran 𝐹𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓))
Theorem	rexrnmpt2 5798*	A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ (𝑧 = 𝐶 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → (∃𝑧 ∈ ran 𝐹𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓))
Theorem	ovid 5799*	The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃!𝑧𝜑)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}    ⇒   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = 𝑧 ↔ 𝜑))
Theorem	ovidig 5800*	The value of an operation class abstraction. Compare ovidi 5801. The condition (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ ∃*𝑧𝜑    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}    ⇒   ⊢ (𝜑 → (𝑥𝐹𝑦) = 𝑧)