P. 76 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7501-7600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ovig 7501*	The value of an operation class abstraction (weak version). (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.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃*𝑧𝜑)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷) → (𝜓 → (𝐴𝐹𝐵) = 𝐶))
Theorem	ovmpt4g 7502*	Value of a function given by the maps-to notation. (This is the operation analogue of fvmpt2 6959.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) = 𝐶)
Theorem	ovmpos 7503*	Value of a function given by the maps-to notation, expressed using explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝑅 ∈ 𝑉) → (𝐴𝐹𝐵) = ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝑅)
Theorem	ov2gf 7504*	The value of an operation class abstraction. A version of ovmpog 7514 using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐺    &   ⊢ Ⅎ𝑦𝑆    &   ⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺)    &   ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpodxf 7505*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐿)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑆    &   ⊢ Ⅎ𝑦𝑆    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpodx 7506*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐿)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpod 7507*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpox 7508*	The value of an operation class abstraction. Variant of ovmpoga 7509 which does not require 𝐷 and 𝑥 to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)    &   ⊢ (𝑥 = 𝐴 → 𝐷 = 𝐿)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpoga 7509*	Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpoa 7510*	Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpodf 7511*	Alternate deduction version of ovmpo 7515, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅 → 𝜓))    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝐹    &   ⊢ Ⅎ𝑦𝜓    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓))
Theorem	ovmpodv 7512*	Alternate deduction version of ovmpo 7515, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅 → 𝜓))    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓))
Theorem	ovmpodv2 7513*	Alternate deduction version of ovmpo 7515, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → (𝐴𝐹𝐵) = 𝑆))
Theorem	ovmpog 7514*	Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺)    &   ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpo 7515*	Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺)    &   ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)
Theorem	fvmpopr2d 7516*	Value of an operation given by maps-to notation. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ (𝜑 → 𝐹 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶))    &   ⊢ (𝜑 → 𝑃 = ⟨𝑎, 𝑏⟩)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐶 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑃) = 𝐶)
Theorem	ov3 7517*	The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 ∈ V    &   ⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 𝑅 = 𝑆)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}    ⇒   ⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (⟨𝐴, 𝐵⟩𝐹⟨𝐶, 𝐷⟩) = 𝑆)
Theorem	ov6g 7518*	The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006.)
⊢ (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑅 = 𝑆)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅)}    ⇒   ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐶) ∧ 𝑆 ∈ 𝐽) → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovg 7519*	The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ ((𝜏 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)) → ∃!𝑧𝜑)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}    ⇒   ⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → ((𝐴𝐹𝐵) = 𝐶 ↔ 𝜃))
Theorem	ovres 7520	The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵))
Theorem	ovresd 7521	Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))
Theorem	oprres 7522*	The restriction of an operation is an operation. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 19-Oct-2021.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐹:(𝑌 × 𝑌)⟶𝑅)    &   ⊢ (𝜑 → 𝐺:(𝑋 × 𝑋)⟶𝑆)    ⇒   ⊢ (𝜑 → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌)))
Theorem	oprssov 7523	The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007.)
⊢ (((Fun 𝐹 ∧ 𝐺 Fn (𝐶 × 𝐷) ∧ 𝐺 ⊆ 𝐹) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Theorem	fovcdm 7524	An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.)
⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
Theorem	fovcdmda 7525	An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶)
Theorem	fovcdmd 7526	An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶)
Theorem	fnrnov 7527*	The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006.)
⊢ (𝐹 Fn (𝐴 × 𝐵) → ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑥𝐹𝑦)})
Theorem	foov 7528*	An onto mapping of an operation expressed in terms of operation values. (Contributed by NM, 29-Oct-2006.)
⊢ (𝐹:(𝐴 × 𝐵)–onto→𝐶 ↔ (𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑧 ∈ 𝐶 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑥𝐹𝑦)))
Theorem	fnovrn 7529	An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007.)
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶𝐹𝐷) ∈ ran 𝐹)
Theorem	ovelrn 7530*	A member of an operation's range is a value of the operation. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
⊢ (𝐹 Fn (𝐴 × 𝐵) → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥𝐹𝑦)))
Theorem	funimassov 7531*	Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
⊢ ((Fun 𝐹 ∧ (𝐴 × 𝐵) ⊆ dom 𝐹) → ((𝐹 “ (𝐴 × 𝐵)) ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶))
Theorem	ovelimab 7532*	Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
⊢ ((𝐹 Fn 𝐴 ∧ (𝐵 × 𝐶) ⊆ 𝐴) → (𝐷 ∈ (𝐹 “ (𝐵 × 𝐶)) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐷 = (𝑥𝐹𝑦)))
Theorem	ovima0 7533	An operation value is a member of the image plus null. (Contributed by Thierry Arnoux, 25-Jun-2019.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝑅𝑌) ∈ ((𝑅 “ (𝐴 × 𝐵)) ∪ {∅}))
Theorem	ovconst2 7534	The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
⊢ 𝐶 ∈ V    ⇒   ⊢ ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵) → (𝑅((𝐴 × 𝐵) × {𝐶})𝑆) = 𝐶)
Theorem	oprssdm 7535*	Domain of closure of an operation. (Contributed by NM, 24-Aug-1995.)
⊢ ¬ ∅ ∈ 𝑆    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥𝐹𝑦) ∈ 𝑆)    ⇒   ⊢ (𝑆 × 𝑆) ⊆ dom 𝐹
Theorem	nssdmovg 7536	The value of an operation outside its domain. (Contributed by Alexander van der Vekens, 7-Sep-2017.)
⊢ ((dom 𝐹 ⊆ (𝑅 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = ∅)
Theorem	ndmovg 7537	The value of an operation outside its domain. (Contributed by NM, 28-Mar-2008.)
⊢ ((dom 𝐹 = (𝑅 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = ∅)
Theorem	ndmov 7538	The value of an operation outside its domain. (Contributed by NM, 24-Aug-1995.)
⊢ dom 𝐹 = (𝑆 × 𝑆)    ⇒   ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) = ∅)
Theorem	ndmovcl 7539	The closure of an operation outside its domain, when the domain includes the empty set. This technical lemma can make the operation more convenient to work in some cases. It is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by NM, 24-Sep-2004.)
⊢ dom 𝐹 = (𝑆 × 𝑆)    &   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝑆)    &   ⊢ ∅ ∈ 𝑆    ⇒   ⊢ (𝐴𝐹𝐵) ∈ 𝑆
Theorem	ndmovrcl 7540	Reverse closure law, when an operation's domain doesn't contain the empty set. (Contributed by NM, 3-Feb-1996.)
⊢ dom 𝐹 = (𝑆 × 𝑆)    &   ⊢ ¬ ∅ ∈ 𝑆    ⇒   ⊢ ((𝐴𝐹𝐵) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆))
Theorem	ndmovcom 7541	Any operation is commutative outside its domain. (Contributed by NM, 24-Aug-1995.)
⊢ dom 𝐹 = (𝑆 × 𝑆)    ⇒   ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) = (𝐵𝐹𝐴))
Theorem	ndmovass 7542	Any operation is associative outside its domain, if the domain doesn't contain the empty set. (Contributed by NM, 24-Aug-1995.)
⊢ dom 𝐹 = (𝑆 × 𝑆)    &   ⊢ ¬ ∅ ∈ 𝑆    ⇒   ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶)))
Theorem	ndmovdistr 7543	Any operation is distributive outside its domain, if the domain doesn't contain the empty set. (Contributed by NM, 24-Aug-1995.)
⊢ dom 𝐹 = (𝑆 × 𝑆)    &   ⊢ ¬ ∅ ∈ 𝑆    &   ⊢ dom 𝐺 = (𝑆 × 𝑆)    ⇒   ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐹(𝐴𝐺𝐶)))
Theorem	ndmovord 7544	Elimination of redundant antecedents in an ordering law. (Contributed by NM, 7-Mar-1996.)
⊢ dom 𝐹 = (𝑆 × 𝑆)    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    &   ⊢ ¬ ∅ ∈ 𝑆    &   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))    ⇒   ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))
Theorem	ndmovordi 7545	Elimination of redundant antecedent in an ordering law. (Contributed by NM, 25-Jun-1998.)
⊢ dom 𝐹 = (𝑆 × 𝑆)    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    &   ⊢ ¬ ∅ ∈ 𝑆    &   ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))    ⇒   ⊢ ((𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵) → 𝐴𝑅𝐵)
2.3.19.1  Variable-to-class conversion for operations
Theorem	caovclg 7546*	Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥𝐹𝑦) ∈ 𝐸)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) → (𝐴𝐹𝐵) ∈ 𝐸)
Theorem	caovcld 7547*	Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥𝐹𝑦) ∈ 𝐸)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐸)
Theorem	caovcl 7548*	Convert an operation closure law to class notation. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥𝐹𝑦) ∈ 𝑆)    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝑆)
Theorem	caovcomg 7549*	Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = (𝐵𝐹𝐴))
Theorem	caovcomd 7550*	Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = (𝐵𝐹𝐴))
Theorem	caovcom 7551*	Convert an operation commutative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    ⇒   ⊢ (𝐴𝐹𝐵) = (𝐵𝐹𝐴)
Theorem	caovassg 7552*	Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro, 26-May-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶)))
Theorem	caovassd 7553*	Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶)))
Theorem	caovass 7554*	Convert an operation associative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))    ⇒   ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))
Theorem	caovcang 7555*	Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) ↔ 𝐵 = 𝐶))
Theorem	caovcand 7556*	Convert an operation cancellation law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) ↔ 𝐵 = 𝐶))
Theorem	caovcanrd 7557*	Commute the arguments of an operation cancellation law. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    ⇒   ⊢ (𝜑 → ((𝐵𝐹𝐴) = (𝐶𝐹𝐴) ↔ 𝐵 = 𝐶))
Theorem	caovcan 7558*	Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.)
⊢ 𝐶 ∈ V    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) → 𝑦 = 𝑧))    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) → 𝐵 = 𝐶))
Theorem	caovordig 7559*	Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 → (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝑅𝐵 → (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))
Theorem	caovordid 7560*	Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 → (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 → (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))
Theorem	caovordg 7561*	Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))
Theorem	caovordd 7562*	Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))
Theorem	caovord2d 7563*	Operation ordering law with commuted arguments. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶)))
Theorem	caovord3d 7564*	Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ⊢ (𝜑 → 𝐷 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐴𝐹𝐵) = (𝐶𝐹𝐷) → (𝐴𝑅𝐶 ↔ 𝐷𝑅𝐵)))
Theorem	caovord 7565*	Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    ⇒   ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))
Theorem	caovord2 7566*	Operation ordering law with commuted arguments. (Contributed by NM, 27-Feb-1996.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    ⇒   ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶)))
Theorem	caovord3 7567*	Ordering law. (Contributed by NM, 29-Feb-1996.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴𝐹𝐵) = (𝐶𝐹𝐷)) → (𝐴𝑅𝐶 ↔ 𝐷𝑅𝐵))
Theorem	caovdig 7568*	Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐻(𝑥𝐺𝑧)))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐻(𝐴𝐺𝐶)))
Theorem	caovdid 7569*	Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐻(𝑥𝐺𝑧)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐻(𝐴𝐺𝐶)))
Theorem	caovdir2d 7570*	Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))    ⇒   ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐶)))
Theorem	caovdirg 7571*	Convert an operation reverse distributive law to class notation. (Contributed by Mario Carneiro, 19-Oct-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧)))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐾)) → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶)))
Theorem	caovdird 7572*	Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶)))
Theorem	caovdi 7573*	Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 28-Jun-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧))    ⇒   ⊢ (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐹(𝐴𝐺𝐶))
Theorem	caov32d 7574*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    ⇒   ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐴𝐹𝐶)𝐹𝐵))
Theorem	caov12d 7575*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    ⇒   ⊢ (𝜑 → (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶)))
Theorem	caov31d 7576*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    ⇒   ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐶𝐹𝐵)𝐹𝐴))
Theorem	caov13d 7577*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    ⇒   ⊢ (𝜑 → (𝐴𝐹(𝐵𝐹𝐶)) = (𝐶𝐹(𝐵𝐹𝐴)))
Theorem	caov4d 7578*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   ⊢ (𝜑 → 𝐷 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷)))
Theorem	caov411d 7579*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   ⊢ (𝜑 → 𝐷 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐶𝐹𝐵)𝐹(𝐴𝐹𝐷)))
Theorem	caov42d 7580*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   ⊢ (𝜑 → 𝐷 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐷𝐹𝐵)))
Theorem	caov32 7581*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))    ⇒   ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐴𝐹𝐶)𝐹𝐵)
Theorem	caov12 7582*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))    ⇒   ⊢ (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶))
Theorem	caov31 7583*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))    ⇒   ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐶𝐹𝐵)𝐹𝐴)
Theorem	caov13 7584*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))    ⇒   ⊢ (𝐴𝐹(𝐵𝐹𝐶)) = (𝐶𝐹(𝐵𝐹𝐴))
Theorem	caov4 7585*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷))
Theorem	caov411 7586*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐶𝐹𝐵)𝐹(𝐴𝐹𝐷))
Theorem	caov42 7587*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐷𝐹𝐵))
Theorem	caovdir 7588*	Reverse distributive law. (Contributed by NM, 26-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥𝐺𝑦) = (𝑦𝐺𝑥)    &   ⊢ (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧))    ⇒   ⊢ ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐶))
Theorem	caovdilem 7589*	Lemma used by real number construction. (Contributed by NM, 26-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥𝐺𝑦) = (𝑦𝐺𝑥)    &   ⊢ (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧))    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐻 ∈ V    &   ⊢ ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))    ⇒   ⊢ (((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻) = ((𝐴𝐺(𝐶𝐺𝐻))𝐹(𝐵𝐺(𝐷𝐺𝐻)))
Theorem	caovlem2 7590*	Lemma used in real number construction. (Contributed by NM, 26-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥𝐺𝑦) = (𝑦𝐺𝑥)    &   ⊢ (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧))    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐻 ∈ V    &   ⊢ ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))    &   ⊢ 𝑅 ∈ V    &   ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))    ⇒   ⊢ ((((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻)𝐹(((𝐴𝐺𝐷)𝐹(𝐵𝐺𝐶))𝐺𝑅)) = ((𝐴𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(𝐵𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻))))
Theorem	caovmo 7591*	Uniqueness of inverse element in commutative, associative operation with identity. Remark in proof of Proposition 9-2.4 of [Gleason] p. 119. (Contributed by NM, 4-Mar-1996.)
⊢ 𝐵 ∈ 𝑆    &   ⊢ dom 𝐹 = (𝑆 × 𝑆)    &   ⊢ ¬ ∅ ∈ 𝑆    &   ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))    &   ⊢ (𝑥 ∈ 𝑆 → (𝑥𝐹𝐵) = 𝑥)    ⇒   ⊢ ∃*𝑤(𝐴𝐹𝑤) = 𝐵
Theorem	imaeqexov 7592*	Substitute an operation value into an existential quantifier over an image. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ (𝑥 = (𝑦𝐹𝑧) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ (𝐵 × 𝐶) ⊆ 𝐴) → (∃𝑥 ∈ (𝐹 “ (𝐵 × 𝐶))𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜓))
Theorem	imaeqalov 7593*	Substitute an operation value into a universal quantifier over an image. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ (𝑥 = (𝑦𝐹𝑧) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ (𝐵 × 𝐶) ⊆ 𝐴) → (∀𝑥 ∈ (𝐹 “ (𝐵 × 𝐶))𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓))
2.3.20  Maps-to notation
Theorem	mpondm0 7594*	The value of an operation given by a maps-to rule is the empty set if the arguments are not contained in the base sets of the rule. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)    ⇒   ⊢ (¬ (𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉𝐹𝑊) = ∅)
Theorem	elmpocl 7595*	If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵))
Theorem	elmpocl1 7596*	If a two-parameter class is not empty, the first argument is in its nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan O'Rear, 7-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → 𝑆 ∈ 𝐴)
Theorem	elmpocl2 7597*	If a two-parameter class is not empty, the second argument is in its nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan O'Rear, 7-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → 𝑇 ∈ 𝐵)
Theorem	elovmpo 7598*	Utility lemma for two-parameter classes. EDITORIAL: can simplify isghm 19008, islmhm 20488. (Contributed by Stefan O'Rear, 21-Jan-2015.)
⊢ 𝐷 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)    &   ⊢ 𝐶 ∈ V    &   ⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → 𝐶 = 𝐸)    ⇒   ⊢ (𝐹 ∈ (𝑋𝐷𝑌) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 ∈ 𝐸))
Theorem	elovmporab 7599*	Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∈ 𝑀 ∣ 𝜑})    &   ⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → 𝑀 ∈ V)    ⇒   ⊢ (𝑍 ∈ (𝑋𝑂𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀))
Theorem	elovmporab1w 7600*	Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. Here, the base set of the class abstraction depends on the first operand. Version of elovmporab1 7601 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by Alexander van der Vekens, 15-Jul-2018.) Avoid ax-13 2370. (Revised by Gino Giotto, 26-Jan-2024.)
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑})    &   ⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → ⦋𝑋 / 𝑚⦌𝑀 ∈ V)    ⇒   ⊢ (𝑍 ∈ (𝑋𝑂𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋𝑋 / 𝑚⦌𝑀))