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	oprabbidv 5501*	Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → {⟨⟨x, y⟩, z⟩ ∣ ψ} = {⟨⟨x, y⟩, z⟩ ∣ χ})
Theorem	oprabbii 5502*	Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (φ ↔ ψ)    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, z⟩ ∣ ψ}
Theorem	ssoprab2 5503	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 4003. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ (∀x∀y∀z(φ → ψ) → {⟨⟨x, y⟩, z⟩ ∣ φ} ⊆ {⟨⟨x, y⟩, z⟩ ∣ ψ})
Theorem	ssoprab2b 5504	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 4004. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ ({⟨⟨x, y⟩, z⟩ ∣ φ} ⊆ {⟨⟨x, y⟩, z⟩ ∣ ψ} ↔ ∀x∀y∀z(φ → ψ))
Theorem	eqoprab2b 5505	Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 4007. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ({⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, z⟩ ∣ ψ} ↔ ∀x∀y∀z(φ ↔ ψ))
Theorem	mpt2eq123 5506*	An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
⊢ ((A = 𝐷 ∧ ∀x ∈ A (B = 𝐸 ∧ ∀y ∈ B 𝐶 = 𝐹)) → (x ∈ A, y ∈ B ↦ 𝐶) = (x ∈ 𝐷, y ∈ 𝐸 ↦ 𝐹))
Theorem	mpt2eq12 5507*	An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((A = 𝐶 ∧ B = 𝐷) → (x ∈ A, y ∈ B ↦ 𝐸) = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝐸))
Theorem	mpt2eq123dva 5508*	An equality deduction for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (φ → A = 𝐷)    &   ⊢ ((φ ∧ x ∈ A) → B = 𝐸)    &   ⊢ ((φ ∧ (x ∈ A ∧ y ∈ B)) → 𝐶 = 𝐹)    ⇒   ⊢ (φ → (x ∈ A, y ∈ B ↦ 𝐶) = (x ∈ 𝐷, y ∈ 𝐸 ↦ 𝐹))
Theorem	mpt2eq123dv 5509*	An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.)
⊢ (φ → A = 𝐷)    &   ⊢ (φ → B = 𝐸)    &   ⊢ (φ → 𝐶 = 𝐹)    ⇒   ⊢ (φ → (x ∈ A, y ∈ B ↦ 𝐶) = (x ∈ 𝐷, y ∈ 𝐸 ↦ 𝐹))
Theorem	mpt2eq123i 5510	An equality inference for the maps to notation. (Contributed by NM, 15-Jul-2013.)
⊢ A = 𝐷    &   ⊢ B = 𝐸    &   ⊢ 𝐶 = 𝐹    ⇒   ⊢ (x ∈ A, y ∈ B ↦ 𝐶) = (x ∈ 𝐷, y ∈ 𝐸 ↦ 𝐹)
Theorem	mpt2eq3dva 5511*	Slightly more general equality inference for the maps to notation. (Contributed by NM, 17-Oct-2013.)
⊢ ((φ ∧ x ∈ A ∧ y ∈ B) → 𝐶 = 𝐷)    ⇒   ⊢ (φ → (x ∈ A, y ∈ B ↦ 𝐶) = (x ∈ A, y ∈ B ↦ 𝐷))
Theorem	mpt2eq3ia 5512	An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((x ∈ A ∧ y ∈ B) → 𝐶 = 𝐷)    ⇒   ⊢ (x ∈ A, y ∈ B ↦ 𝐶) = (x ∈ A, y ∈ B ↦ 𝐷)
Theorem	nfmpt21 5513	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎx(x ∈ A, y ∈ B ↦ 𝐶)
Theorem	nfmpt22 5514	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎy(x ∈ A, y ∈ B ↦ 𝐶)
Theorem	nfmpt2 5515*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ ℲzA    &   ⊢ ℲzB    &   ⊢ Ⅎz𝐶    ⇒   ⊢ Ⅎz(x ∈ A, y ∈ B ↦ 𝐶)
Theorem	mpt20 5516	A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ (x ∈ ∅, y ∈ B ↦ 𝐶) = ∅
Theorem	oprab4 5517*	Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)
⊢ {⟨⟨x, y⟩, z⟩ ∣ (⟨x, y⟩ ∈ (A × B) ∧ φ)} = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)}
Theorem	cbvoprab1 5518*	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.)
⊢ Ⅎwφ    &   ⊢ Ⅎxψ    &   ⊢ (x = w → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨w, y⟩, z⟩ ∣ ψ}
Theorem	cbvoprab2 5519*	Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎwφ    &   ⊢ Ⅎyψ    &   ⊢ (y = w → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, w⟩, z⟩ ∣ ψ}
Theorem	cbvoprab12 5520*	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 5521*	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 5522*	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 5523*	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 5524*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 5525 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 5525*	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 5526*	Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 3842, 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 5527*	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 5528*	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 5529*	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 5530*	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 5531*	The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)
⊢ Rel dom {⟨⟨x, y⟩, z⟩ ∣ φ}
Theorem	oprabss 5532*	Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)
⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} ⊆ ((V × V) × V)
Theorem	eloprabga 5533*	The law of concretion for operation class abstraction. Compare elopab 3986. (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 5534*	The law of concretion for operation class abstraction. Compare elopab 3986. (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 5535*	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 5536*	Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
⊢ (x ∈ V, y ∈ V ↦ 𝐶) = {⟨⟨x, y⟩, z⟩ ∣ z = 𝐶}
Theorem	mpt2mptx 5537*	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 5538*	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 5539*	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 5540*	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 5541*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)
⊢ ((𝐶 ⊆ A ∧ 𝐷 ⊆ B) → ((x ∈ A, y ∈ B ↦ 𝐸) ↾ (𝐶 × 𝐷)) = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝐸))
Theorem	funoprabg 5542*	"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 5543*	"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 5544*	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 5545*	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 5546*	Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995.)
⊢ (φ → ∃!zψ)    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ (φ ∧ ψ)} Fn {⟨x, y⟩ ∣ φ}
Theorem	ffnov 5547*	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 5548	Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶    ⇒   ⊢ ((A ∈ 𝑅 ∧ B ∈ 𝑆) → (A𝐹B) ∈ 𝐶)
Theorem	eqfnov 5549*	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 5550*	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 5551*	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 5552*	Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 5550. (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 5553*	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 5554*	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 5555*	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 5556*	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 5557*	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 5558*	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 5559*	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 5560*	The value of an operation class abstraction. Compare ovidi 5561. The condition (x ∈ 𝑅 ∧ y ∈ 𝑆) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ ∃*zφ    &   ⊢ 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ φ}    ⇒   ⊢ (φ → (x𝐹y) = z)
Theorem	ovidi 5561*	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 5562*	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 5563*	The value of an operation class abstraction. Compare ovig 5564. 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 5564*	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 5565*	Value of a function given by the "maps to" notation. (This is the operation analog of fvmpt2 5197.) (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 5566*	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 5567*	The value of an operation class abstraction. A version of ovmpt2g 5577 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 5568*	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 5569*	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 5570*	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 5571*	The value of an operation class abstraction. Variant of ovmpt2ga 5572 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 5572*	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 5573*	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 5574*	Alternate deduction version of ovmpt2 5578, 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 5575*	Alternate deduction version of ovmpt2 5578, 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 5576*	Alternate deduction version of ovmpt2 5578, 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 5577*	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 5578*	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 5579*	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 5580*	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 5581*	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 5582	The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷) → (A(𝐹 ↾ (𝐶 × 𝐷))B) = (A𝐹B))
Theorem	ovresd 5583	Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (φ → A ∈ 𝑋)    &   ⊢ (φ → B ∈ 𝑋)    ⇒   ⊢ (φ → (A(𝐷 ↾ (𝑋 × 𝑋))B) = (A𝐷B))
Theorem	oprssov 5584	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 5585	An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.)
⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ A ∈ 𝑅 ∧ B ∈ 𝑆) → (A𝐹B) ∈ 𝐶)
Theorem	fovrnda 5586	An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (φ → 𝐹:(𝑅 × 𝑆)⟶𝐶)    ⇒   ⊢ ((φ ∧ (A ∈ 𝑅 ∧ B ∈ 𝑆)) → (A𝐹B) ∈ 𝐶)
Theorem	fovrnd 5587	An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (φ → 𝐹:(𝑅 × 𝑆)⟶𝐶)    &   ⊢ (φ → A ∈ 𝑅)    &   ⊢ (φ → B ∈ 𝑆)    ⇒   ⊢ (φ → (A𝐹B) ∈ 𝐶)
Theorem	fnrnov 5588*	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 5589*	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 5590	An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007.)
⊢ ((𝐹 Fn (A × B) ∧ 𝐶 ∈ A ∧ 𝐷 ∈ B) → (𝐶𝐹𝐷) ∈ ran 𝐹)
Theorem	ovelrn 5591*	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 5592*	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 5593*	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 5594	The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
⊢ 𝐶 ∈ V    ⇒   ⊢ ((𝑅 ∈ A ∧ 𝑆 ∈ B) → (𝑅((A × B) × {𝐶})𝑆) = 𝐶)
Theorem	caovclg 5595*	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 5596*	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 5597*	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 5598*	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 5599*	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 5600*	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)