P. 56 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5501-5600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cbvoprab12 5501*	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.)
⊢ Ⅎwφ    &   ⊢ Ⅎvφ    &   ⊢ Ⅎxψ    &   ⊢ Ⅎyψ    &   ⊢ ((x = w ∧ y = v) → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨w, v⟩, z⟩ ∣ ψ}
Theorem	cbvoprab12v 5502*	Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.)
⊢ ((x = w ∧ y = v) → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨w, v⟩, z⟩ ∣ ψ}
Theorem	cbvoprab3 5503*	Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎwφ    &   ⊢ Ⅎzψ    &   ⊢ (z = w → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, w⟩ ∣ ψ}
Theorem	cbvoprab3v 5504*	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.)
⊢ (z = w → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, w⟩ ∣ ψ}
Theorem	cbvmpt2x 5505*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 5506 allows B to be a function of x. (Contributed by NM, 29-Dec-2014.)
⊢ ℲzB    &   ⊢ Ⅎx𝐷    &   ⊢ Ⅎz𝐶    &   ⊢ Ⅎw𝐶    &   ⊢ Ⅎx𝐸    &   ⊢ Ⅎy𝐸    &   ⊢ (x = z → B = 𝐷)    &   ⊢ ((x = z ∧ y = w) → 𝐶 = 𝐸)    ⇒   ⊢ (x ∈ A, y ∈ B ↦ 𝐶) = (z ∈ A, w ∈ 𝐷 ↦ 𝐸)
Theorem	cbvmpt2 5506*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.)
⊢ Ⅎz𝐶    &   ⊢ Ⅎw𝐶    &   ⊢ Ⅎx𝐷    &   ⊢ Ⅎy𝐷    &   ⊢ ((x = z ∧ y = w) → 𝐶 = 𝐷)    ⇒   ⊢ (x ∈ A, y ∈ B ↦ 𝐶) = (z ∈ A, w ∈ B ↦ 𝐷)
Theorem	cbvmpt2v 5507*	Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 3825, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)
⊢ (x = z → 𝐶 = 𝐸)    &   ⊢ (y = w → 𝐸 = 𝐷)    ⇒   ⊢ (x ∈ A, y ∈ B ↦ 𝐶) = (z ∈ A, w ∈ B ↦ 𝐷)
Theorem	dmoprab 5508*	The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ dom {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨x, y⟩ ∣ ∃zφ}
Theorem	dmoprabss 5509*	The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995.)
⊢ dom {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} ⊆ (A × B)
Theorem	rnoprab 5510*	The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)
⊢ ran {⟨⟨x, y⟩, z⟩ ∣ φ} = {z ∣ ∃x∃yφ}
Theorem	rnoprab2 5511*	The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.)
⊢ ran {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} = {z ∣ ∃x ∈ A ∃y ∈ B φ}
Theorem	reldmoprab 5512*	The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)
⊢ Rel dom {⟨⟨x, y⟩, z⟩ ∣ φ}
Theorem	oprabss 5513*	Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)
⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} ⊆ ((V × V) × V)
Theorem	eloprabga 5514*	The law of concretion for operation class abstraction. Compare elopab 3969. (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.)
⊢ ((x = A ∧ y = B ∧ z = 𝐶) → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨⟨A, B⟩, 𝐶⟩ ∈ {⟨⟨x, y⟩, z⟩ ∣ φ} ↔ ψ))
Theorem	eloprabg 5515*	The law of concretion for operation class abstraction. Compare elopab 3969. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (z = 𝐶 → (χ ↔ θ))    ⇒   ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨⟨A, B⟩, 𝐶⟩ ∈ {⟨⟨x, y⟩, z⟩ ∣ φ} ↔ θ))
Theorem	ssoprab2i 5516*	Inference of operation class abstraction subclass from implication. (Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (φ → ψ)    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} ⊆ {⟨⟨x, y⟩, z⟩ ∣ ψ}
Theorem	mpt2v 5517*	Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
⊢ (x ∈ V, y ∈ V ↦ 𝐶) = {⟨⟨x, y⟩, z⟩ ∣ z = 𝐶}
Theorem	mpt2mptx 5518*	Express a two-argument function as a one-argument function, or vice-versa. In this version B(x) is not assumed to be constant w.r.t x. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (z = ⟨x, y⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (z ∈ ∪ x ∈ A ({x} × B) ↦ 𝐶) = (x ∈ A, y ∈ B ↦ 𝐷)
Theorem	mpt2mpt 5519*	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.)
⊢ (z = ⟨x, y⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (z ∈ (A × B) ↦ 𝐶) = (x ∈ A, y ∈ B ↦ 𝐷)
Theorem	resoprab 5520*	Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007.)
⊢ ({⟨⟨x, y⟩, z⟩ ∣ φ} ↾ (A × B)) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)}
Theorem	resoprab2 5521*	Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐶 ⊆ A ∧ 𝐷 ⊆ B) → ({⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} ↾ (𝐶 × 𝐷)) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ 𝐶 ∧ y ∈ 𝐷) ∧ φ)})
Theorem	resmpt2 5522*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)
⊢ ((𝐶 ⊆ A ∧ 𝐷 ⊆ B) → ((x ∈ A, y ∈ B ↦ 𝐸) ↾ (𝐶 × 𝐷)) = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝐸))
Theorem	funoprabg 5523*	"At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 28-Aug-2007.)
⊢ (∀x∀y∃*zφ → Fun {⟨⟨x, y⟩, z⟩ ∣ φ})
Theorem	funoprab 5524*	"At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 17-Mar-1995.)
⊢ ∃*zφ    ⇒   ⊢ Fun {⟨⟨x, y⟩, z⟩ ∣ φ}
Theorem	fnoprabg 5525*	Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007.)
⊢ (∀x∀y(φ → ∃!zψ) → {⟨⟨x, y⟩, z⟩ ∣ (φ ∧ ψ)} Fn {⟨x, y⟩ ∣ φ})
Theorem	mpt2fun 5526*	The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.)
⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)    ⇒   ⊢ Fun 𝐹
Theorem	fnoprab 5527*	Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995.)
⊢ (φ → ∃!zψ)    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ (φ ∧ ψ)} Fn {⟨x, y⟩ ∣ φ}
Theorem	ffnov 5528*	An operation maps to a class to which all values belong. (Contributed by NM, 7-Feb-2004.)
⊢ (𝐹:(A × B)⟶𝐶 ↔ (𝐹 Fn (A × B) ∧ ∀x ∈ A ∀y ∈ B (x𝐹y) ∈ 𝐶))
Theorem	fovcl 5529	Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶    ⇒   ⊢ ((A ∈ 𝑅 ∧ B ∈ 𝑆) → (A𝐹B) ∈ 𝐶)
Theorem	eqfnov 5530*	Equality of two operations is determined by their values. (Contributed by NM, 1-Sep-2005.)
⊢ ((𝐹 Fn (A × B) ∧ 𝐺 Fn (𝐶 × 𝐷)) → (𝐹 = 𝐺 ↔ ((A × B) = (𝐶 × 𝐷) ∧ ∀x ∈ A ∀y ∈ B (x𝐹y) = (x𝐺y))))
Theorem	eqfnov2 5531*	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 (A × B) ∧ 𝐺 Fn (A × B)) → (𝐹 = 𝐺 ↔ ∀x ∈ A ∀y ∈ B (x𝐹y) = (x𝐺y)))
Theorem	fnovim 5532*	Representation of a function in terms of its values. (Contributed by Jim Kingdon, 16-Jan-2019.)
⊢ (𝐹 Fn (A × B) → 𝐹 = (x ∈ A, y ∈ B ↦ (x𝐹y)))
Theorem	mpt22eqb 5533*	Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 5531. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝑉 → ((x ∈ A, y ∈ B ↦ 𝐶) = (x ∈ A, y ∈ B ↦ 𝐷) ↔ ∀x ∈ A ∀y ∈ B 𝐶 = 𝐷))
Theorem	rnmpt2 5534*	The range of an operation given by the "maps to" notation. (Contributed by FL, 20-Jun-2011.)
⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)    ⇒   ⊢ ran 𝐹 = {z ∣ ∃x ∈ A ∃y ∈ B z = 𝐶}
Theorem	reldmmpt2 5535*	The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)    ⇒   ⊢ Rel dom 𝐹
Theorem	elrnmpt2g 5536*	Membership in the range of an operation class abstraction. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)    ⇒   ⊢ (𝐷 ∈ 𝑉 → (𝐷 ∈ ran 𝐹 ↔ ∃x ∈ A ∃y ∈ B 𝐷 = 𝐶))
Theorem	elrnmpt2 5537*	Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐷 ∈ ran 𝐹 ↔ ∃x ∈ A ∃y ∈ B 𝐷 = 𝐶)
Theorem	ralrnmpt2 5538*	A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)    &   ⊢ (z = 𝐶 → (φ ↔ ψ))    ⇒   ⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝑉 → (∀z ∈ ran 𝐹φ ↔ ∀x ∈ A ∀y ∈ B ψ))
Theorem	rexrnmpt2 5539*	A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)    &   ⊢ (z = 𝐶 → (φ ↔ ψ))    ⇒   ⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝑉 → (∃z ∈ ran 𝐹φ ↔ ∃x ∈ A ∃y ∈ B ψ))
Theorem	ovid 5540*	The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ ((x ∈ 𝑅 ∧ y ∈ 𝑆) → ∃!zφ)    &   ⊢ 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)}    ⇒   ⊢ ((x ∈ 𝑅 ∧ y ∈ 𝑆) → ((x𝐹y) = z ↔ φ))
Theorem	ovidig 5541*	The value of an operation class abstraction. Compare ovidi 5542. The condition (x ∈ 𝑅 ∧ y ∈ 𝑆) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ ∃*zφ    &   ⊢ 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ φ}    ⇒   ⊢ (φ → (x𝐹y) = z)
Theorem	ovidi 5542*	The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ ((x ∈ 𝑅 ∧ y ∈ 𝑆) → ∃*zφ)    &   ⊢ 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)}    ⇒   ⊢ ((x ∈ 𝑅 ∧ y ∈ 𝑆) → (φ → (x𝐹y) = z))
Theorem	ov 5543*	The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ 𝐶 ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (z = 𝐶 → (χ ↔ θ))    &   ⊢ ((x ∈ 𝑅 ∧ y ∈ 𝑆) → ∃!zφ)    &   ⊢ 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)}    ⇒   ⊢ ((A ∈ 𝑅 ∧ B ∈ 𝑆) → ((A𝐹B) = 𝐶 ↔ θ))
Theorem	ovigg 5544*	The value of an operation class abstraction. Compare ovig 5545. The condition (x ∈ 𝑅 ∧ y ∈ 𝑆) is been removed. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ ((x = A ∧ y = B ∧ z = 𝐶) → (φ ↔ ψ))    &   ⊢ ∃*zφ    &   ⊢ 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ φ}    ⇒   ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (ψ → (A𝐹B) = 𝐶))
Theorem	ovig 5545*	The value of an operation class abstraction (weak version). (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 14-Sep-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ ((x = A ∧ y = B ∧ z = 𝐶) → (φ ↔ ψ))    &   ⊢ ((x ∈ 𝑅 ∧ y ∈ 𝑆) → ∃*zφ)    &   ⊢ 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)}    ⇒   ⊢ ((A ∈ 𝑅 ∧ B ∈ 𝑆 ∧ 𝐶 ∈ 𝐷) → (ψ → (A𝐹B) = 𝐶))
Theorem	ovmpt4g 5546*	Value of a function given by the "maps to" notation. (This is the operation analog of fvmpt2 5179.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)    ⇒   ⊢ ((x ∈ A ∧ y ∈ B ∧ 𝐶 ∈ 𝑉) → (x𝐹y) = 𝐶)
Theorem	ovmpt2s 5547*	Value of a function given by the "maps to" notation, expressed using explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷 ∧ ⦋A / x⦌⦋B / y⦌𝑅 ∈ 𝑉) → (A𝐹B) = ⦋A / x⦌⦋B / y⦌𝑅)
Theorem	ov2gf 5548*	The value of an operation class abstraction. A version of ovmpt2g 5558 using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ ℲxA    &   ⊢ ℲyA    &   ⊢ ℲyB    &   ⊢ Ⅎx𝐺    &   ⊢ Ⅎy𝑆    &   ⊢ (x = A → 𝑅 = 𝐺)    &   ⊢ (y = B → 𝐺 = 𝑆)    &   ⊢ 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (A𝐹B) = 𝑆)
Theorem	ovmpt2dxf 5549*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (φ → 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((φ ∧ (x = A ∧ y = B)) → 𝑅 = 𝑆)    &   ⊢ ((φ ∧ x = A) → 𝐷 = 𝐿)    &   ⊢ (φ → A ∈ 𝐶)    &   ⊢ (φ → B ∈ 𝐿)    &   ⊢ (φ → 𝑆 ∈ 𝑋)    &   ⊢ Ⅎxφ    &   ⊢ Ⅎyφ    &   ⊢ ℲyA    &   ⊢ ℲxB    &   ⊢ Ⅎx𝑆    &   ⊢ Ⅎy𝑆    ⇒   ⊢ (φ → (A𝐹B) = 𝑆)
Theorem	ovmpt2dx 5550*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (φ → 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((φ ∧ (x = A ∧ y = B)) → 𝑅 = 𝑆)    &   ⊢ ((φ ∧ x = A) → 𝐷 = 𝐿)    &   ⊢ (φ → A ∈ 𝐶)    &   ⊢ (φ → B ∈ 𝐿)    &   ⊢ (φ → 𝑆 ∈ 𝑋)    ⇒   ⊢ (φ → (A𝐹B) = 𝑆)
Theorem	ovmpt2d 5551*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ (φ → 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((φ ∧ (x = A ∧ y = B)) → 𝑅 = 𝑆)    &   ⊢ (φ → A ∈ 𝐶)    &   ⊢ (φ → B ∈ 𝐷)    &   ⊢ (φ → 𝑆 ∈ 𝑋)    ⇒   ⊢ (φ → (A𝐹B) = 𝑆)
Theorem	ovmpt2x 5552*	The value of an operation class abstraction. Variant of ovmpt2ga 5553 which does not require 𝐷 and x to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
⊢ ((x = A ∧ y = B) → 𝑅 = 𝑆)    &   ⊢ (x = A → 𝐷 = 𝐿)    &   ⊢ 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐿 ∧ 𝑆 ∈ 𝐻) → (A𝐹B) = 𝑆)
Theorem	ovmpt2ga 5553*	Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((x = A ∧ y = B) → 𝑅 = 𝑆)    &   ⊢ 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (A𝐹B) = 𝑆)
Theorem	ovmpt2a 5554*	Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.)
⊢ ((x = A ∧ y = B) → 𝑅 = 𝑆)    &   ⊢ 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷) → (A𝐹B) = 𝑆)
Theorem	ovmpt2df 5555*	Alternate deduction version of ovmpt2 5559, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (φ → A ∈ 𝐶)    &   ⊢ ((φ ∧ x = A) → B ∈ 𝐷)    &   ⊢ ((φ ∧ (x = A ∧ y = B)) → 𝑅 ∈ 𝑉)    &   ⊢ ((φ ∧ (x = A ∧ y = B)) → ((A𝐹B) = 𝑅 → ψ))    &   ⊢ Ⅎx𝐹    &   ⊢ Ⅎxψ    &   ⊢ Ⅎy𝐹    &   ⊢ Ⅎyψ    ⇒   ⊢ (φ → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ))
Theorem	ovmpt2dv 5556*	Alternate deduction version of ovmpt2 5559, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (φ → A ∈ 𝐶)    &   ⊢ ((φ ∧ x = A) → B ∈ 𝐷)    &   ⊢ ((φ ∧ (x = A ∧ y = B)) → 𝑅 ∈ 𝑉)    &   ⊢ ((φ ∧ (x = A ∧ y = B)) → ((A𝐹B) = 𝑅 → ψ))    ⇒   ⊢ (φ → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ))
Theorem	ovmpt2dv2 5557*	Alternate deduction version of ovmpt2 5559, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (φ → A ∈ 𝐶)    &   ⊢ ((φ ∧ x = A) → B ∈ 𝐷)    &   ⊢ ((φ ∧ (x = A ∧ y = B)) → 𝑅 ∈ 𝑉)    &   ⊢ ((φ ∧ (x = A ∧ y = B)) → 𝑅 = 𝑆)    ⇒   ⊢ (φ → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → (A𝐹B) = 𝑆))
Theorem	ovmpt2g 5558*	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.)
⊢ (x = A → 𝑅 = 𝐺)    &   ⊢ (y = B → 𝐺 = 𝑆)    &   ⊢ 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (A𝐹B) = 𝑆)
Theorem	ovmpt2 5559*	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.)
⊢ (x = A → 𝑅 = 𝐺)    &   ⊢ (y = B → 𝐺 = 𝑆)    &   ⊢ 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷) → (A𝐹B) = 𝑆)
Theorem	ovi3 5560*	The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)
⊢ (((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → 𝑆 ∈ (𝐻 × 𝐻))    &   ⊢ (((w = A ∧ v = B) ∧ (u = 𝐶 ∧ f = 𝐷)) → 𝑅 = 𝑆)    &   ⊢ 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ (𝐻 × 𝐻) ∧ y ∈ (𝐻 × 𝐻)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅))}    ⇒   ⊢ (((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = 𝑆)
Theorem	ov6g 5561*	The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006.)
⊢ (⟨x, y⟩ = ⟨A, B⟩ → 𝑅 = 𝑆)    &   ⊢ 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ (⟨x, y⟩ ∈ 𝐶 ∧ z = 𝑅)}    ⇒   ⊢ (((A ∈ 𝐺 ∧ B ∈ 𝐻 ∧ ⟨A, B⟩ ∈ 𝐶) ∧ 𝑆 ∈ 𝐽) → (A𝐹B) = 𝑆)
Theorem	ovg 5562*	The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (z = 𝐶 → (χ ↔ θ))    &   ⊢ ((τ ∧ (x ∈ 𝑅 ∧ y ∈ 𝑆)) → ∃!zφ)    &   ⊢ 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)}    ⇒   ⊢ ((τ ∧ (A ∈ 𝑅 ∧ B ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → ((A𝐹B) = 𝐶 ↔ θ))
Theorem	ovres 5563	The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷) → (A(𝐹 ↾ (𝐶 × 𝐷))B) = (A𝐹B))
Theorem	ovresd 5564	Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (φ → A ∈ 𝑋)    &   ⊢ (φ → B ∈ 𝑋)    ⇒   ⊢ (φ → (A(𝐷 ↾ (𝑋 × 𝑋))B) = (A𝐷B))
Theorem	oprssov 5565	The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007.)
⊢ (((Fun 𝐹 ∧ 𝐺 Fn (𝐶 × 𝐷) ∧ 𝐺 ⊆ 𝐹) ∧ (A ∈ 𝐶 ∧ B ∈ 𝐷)) → (A𝐹B) = (A𝐺B))
Theorem	fovrn 5566	An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.)
⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ A ∈ 𝑅 ∧ B ∈ 𝑆) → (A𝐹B) ∈ 𝐶)
Theorem	fovrnda 5567	An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (φ → 𝐹:(𝑅 × 𝑆)⟶𝐶)    ⇒   ⊢ ((φ ∧ (A ∈ 𝑅 ∧ B ∈ 𝑆)) → (A𝐹B) ∈ 𝐶)
Theorem	fovrnd 5568	An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (φ → 𝐹:(𝑅 × 𝑆)⟶𝐶)    &   ⊢ (φ → A ∈ 𝑅)    &   ⊢ (φ → B ∈ 𝑆)    ⇒   ⊢ (φ → (A𝐹B) ∈ 𝐶)
Theorem	fnrnov 5569*	The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006.)
⊢ (𝐹 Fn (A × B) → ran 𝐹 = {z ∣ ∃x ∈ A ∃y ∈ B z = (x𝐹y)})
Theorem	foov 5570*	An onto mapping of an operation expressed in terms of operation values. (Contributed by NM, 29-Oct-2006.)
⊢ (𝐹:(A × B)–onto→𝐶 ↔ (𝐹:(A × B)⟶𝐶 ∧ ∀z ∈ 𝐶 ∃x ∈ A ∃y ∈ B z = (x𝐹y)))
Theorem	fnovrn 5571	An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007.)
⊢ ((𝐹 Fn (A × B) ∧ 𝐶 ∈ A ∧ 𝐷 ∈ B) → (𝐶𝐹𝐷) ∈ ran 𝐹)
Theorem	ovelrn 5572*	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 (A × B) → (𝐶 ∈ ran 𝐹 ↔ ∃x ∈ A ∃y ∈ B 𝐶 = (x𝐹y)))
Theorem	funimassov 5573*	Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
⊢ ((Fun 𝐹 ∧ (A × B) ⊆ dom 𝐹) → ((𝐹 “ (A × B)) ⊆ 𝐶 ↔ ∀x ∈ A ∀y ∈ B (x𝐹y) ∈ 𝐶))
Theorem	ovelimab 5574*	Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
⊢ ((𝐹 Fn A ∧ (B × 𝐶) ⊆ A) → (𝐷 ∈ (𝐹 “ (B × 𝐶)) ↔ ∃x ∈ B ∃y ∈ 𝐶 𝐷 = (x𝐹y)))
Theorem	ovconst2 5575	The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
⊢ 𝐶 ∈ V    ⇒   ⊢ ((𝑅 ∈ A ∧ 𝑆 ∈ B) → (𝑅((A × B) × {𝐶})𝑆) = 𝐶)
Theorem	caovclg 5576*	Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.)
⊢ ((φ ∧ (x ∈ 𝐶 ∧ y ∈ 𝐷)) → (x𝐹y) ∈ 𝐸)    ⇒   ⊢ ((φ ∧ (A ∈ 𝐶 ∧ B ∈ 𝐷)) → (A𝐹B) ∈ 𝐸)
Theorem	caovcld 5577*	Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((φ ∧ (x ∈ 𝐶 ∧ y ∈ 𝐷)) → (x𝐹y) ∈ 𝐸)    &   ⊢ (φ → A ∈ 𝐶)    &   ⊢ (φ → B ∈ 𝐷)    ⇒   ⊢ (φ → (A𝐹B) ∈ 𝐸)
Theorem	caovcl 5578*	Convert an operation closure law to class notation. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
⊢ ((x ∈ 𝑆 ∧ y ∈ 𝑆) → (x𝐹y) ∈ 𝑆)    ⇒   ⊢ ((A ∈ 𝑆 ∧ B ∈ 𝑆) → (A𝐹B) ∈ 𝑆)
Theorem	caovcomg 5579*	Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.)
⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) = (y𝐹x))    ⇒   ⊢ ((φ ∧ (A ∈ 𝑆 ∧ B ∈ 𝑆)) → (A𝐹B) = (B𝐹A))
Theorem	caovcomd 5580*	Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) = (y𝐹x))    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ (φ → B ∈ 𝑆)    ⇒   ⊢ (φ → (A𝐹B) = (B𝐹A))
Theorem	caovcom 5581*	Convert an operation commutative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (x𝐹y) = (y𝐹x)    ⇒   ⊢ (A𝐹B) = (B𝐹A)
Theorem	caovassg 5582*	Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro, 26-May-2014.)
⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))    ⇒   ⊢ ((φ ∧ (A ∈ 𝑆 ∧ B ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((A𝐹B)𝐹𝐶) = (A𝐹(B𝐹𝐶)))
Theorem	caovassd 5583*	Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ (φ → B ∈ 𝑆)    &   ⊢ (φ → 𝐶 ∈ 𝑆)    ⇒   ⊢ (φ → ((A𝐹B)𝐹𝐶) = (A𝐹(B𝐹𝐶)))
Theorem	caovass 5584*	Convert an operation associative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ ((x𝐹y)𝐹z) = (x𝐹(y𝐹z))    ⇒   ⊢ ((A𝐹B)𝐹𝐶) = (A𝐹(B𝐹𝐶))
Theorem	caovcang 5585*	Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ ((φ ∧ (x ∈ 𝑇 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐹y) = (x𝐹z) ↔ y = z))    ⇒   ⊢ ((φ ∧ (A ∈ 𝑇 ∧ B ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((A𝐹B) = (A𝐹𝐶) ↔ B = 𝐶))
Theorem	caovcand 5586*	Convert an operation cancellation law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((φ ∧ (x ∈ 𝑇 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐹y) = (x𝐹z) ↔ y = z))    &   ⊢ (φ → A ∈ 𝑇)    &   ⊢ (φ → B ∈ 𝑆)    &   ⊢ (φ → 𝐶 ∈ 𝑆)    ⇒   ⊢ (φ → ((A𝐹B) = (A𝐹𝐶) ↔ B = 𝐶))
Theorem	caovcanrd 5587*	Commute the arguments of an operation cancellation law. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((φ ∧ (x ∈ 𝑇 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐹y) = (x𝐹z) ↔ y = z))    &   ⊢ (φ → A ∈ 𝑇)    &   ⊢ (φ → B ∈ 𝑆)    &   ⊢ (φ → 𝐶 ∈ 𝑆)    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) = (y𝐹x))    ⇒   ⊢ (φ → ((B𝐹A) = (𝐶𝐹A) ↔ B = 𝐶))
Theorem	caovcan 5588*	Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.)
⊢ 𝐶 ∈ V    &   ⊢ ((x ∈ 𝑆 ∧ y ∈ 𝑆) → ((x𝐹y) = (x𝐹z) → y = z))    ⇒   ⊢ ((A ∈ 𝑆 ∧ B ∈ 𝑆) → ((A𝐹B) = (A𝐹𝐶) → B = 𝐶))
Theorem	caovordig 5589*	Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (x𝑅y → (z𝐹x)𝑅(z𝐹y)))    ⇒   ⊢ ((φ ∧ (A ∈ 𝑆 ∧ B ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (A𝑅B → (𝐶𝐹A)𝑅(𝐶𝐹B)))
Theorem	caovordid 5590*	Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (x𝑅y → (z𝐹x)𝑅(z𝐹y)))    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ (φ → B ∈ 𝑆)    &   ⊢ (φ → 𝐶 ∈ 𝑆)    ⇒   ⊢ (φ → (A𝑅B → (𝐶𝐹A)𝑅(𝐶𝐹B)))
Theorem	caovordg 5591*	Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))    ⇒   ⊢ ((φ ∧ (A ∈ 𝑆 ∧ B ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (A𝑅B ↔ (𝐶𝐹A)𝑅(𝐶𝐹B)))
Theorem	caovordd 5592*	Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ (φ → B ∈ 𝑆)    &   ⊢ (φ → 𝐶 ∈ 𝑆)    ⇒   ⊢ (φ → (A𝑅B ↔ (𝐶𝐹A)𝑅(𝐶𝐹B)))
Theorem	caovord2d 5593*	Operation ordering law with commuted arguments. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ (φ → B ∈ 𝑆)    &   ⊢ (φ → 𝐶 ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) = (y𝐹x))    ⇒   ⊢ (φ → (A𝑅B ↔ (A𝐹𝐶)𝑅(B𝐹𝐶)))
Theorem	caovord3d 5594*	Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ (φ → B ∈ 𝑆)    &   ⊢ (φ → 𝐶 ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) = (y𝐹x))    &   ⊢ (φ → 𝐷 ∈ 𝑆)    ⇒   ⊢ (φ → ((A𝐹B) = (𝐶𝐹𝐷) → (A𝑅𝐶 ↔ 𝐷𝑅B)))
Theorem	caovord 5595*	Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (z ∈ 𝑆 → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))    ⇒   ⊢ (𝐶 ∈ 𝑆 → (A𝑅B ↔ (𝐶𝐹A)𝑅(𝐶𝐹B)))
Theorem	caovord2 5596*	Operation ordering law with commuted arguments. (Contributed by NM, 27-Feb-1996.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (z ∈ 𝑆 → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))    &   ⊢ 𝐶 ∈ V    &   ⊢ (x𝐹y) = (y𝐹x)    ⇒   ⊢ (𝐶 ∈ 𝑆 → (A𝑅B ↔ (A𝐹𝐶)𝑅(B𝐹𝐶)))
Theorem	caovord3 5597*	Ordering law. (Contributed by NM, 29-Feb-1996.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (z ∈ 𝑆 → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))    &   ⊢ 𝐶 ∈ V    &   ⊢ (x𝐹y) = (y𝐹x)    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (((B ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (A𝐹B) = (𝐶𝐹𝐷)) → (A𝑅𝐶 ↔ 𝐷𝑅B))
Theorem	caovdig 5598*	Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
⊢ ((φ ∧ (x ∈ 𝐾 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (x𝐺(y𝐹z)) = ((x𝐺y)𝐻(x𝐺z)))    ⇒   ⊢ ((φ ∧ (A ∈ 𝐾 ∧ B ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (A𝐺(B𝐹𝐶)) = ((A𝐺B)𝐻(A𝐺𝐶)))
Theorem	caovdid 5599*	Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((φ ∧ (x ∈ 𝐾 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (x𝐺(y𝐹z)) = ((x𝐺y)𝐻(x𝐺z)))    &   ⊢ (φ → A ∈ 𝐾)    &   ⊢ (φ → B ∈ 𝑆)    &   ⊢ (φ → 𝐶 ∈ 𝑆)    ⇒   ⊢ (φ → (A𝐺(B𝐹𝐶)) = ((A𝐺B)𝐻(A𝐺𝐶)))
Theorem	caovdir2d 5600*	Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (x𝐺(y𝐹z)) = ((x𝐺y)𝐹(x𝐺z)))    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ (φ → B ∈ 𝑆)    &   ⊢ (φ → 𝐶 ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐺y) = (y𝐺x))    ⇒   ⊢ (φ → ((A𝐹B)𝐺𝐶) = ((A𝐺𝐶)𝐹(B𝐺𝐶)))