P. 57 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 5601-5700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ov6g 5601*	The value of an operation class abstraction. Special case. (Contributed by set.mm contributors, 13-Nov-2006.)
⊢ (⟨x, y⟩ = ⟨A, B⟩ → R = S)    &   ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ (⟨x, y⟩ ∈ C ∧ z = R)}    ⇒   ⊢ (((A ∈ G ∧ B ∈ H ∧ ⟨A, B⟩ ∈ C) ∧ S ∈ J) → (AFB) = S)
Theorem	ovg 5602*	The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (z = C → (χ ↔ θ))    &   ⊢ ((τ ∧ (x ∈ R ∧ y ∈ S)) → ∃!zφ)    &   ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ R ∧ y ∈ S) ∧ φ)}    ⇒   ⊢ ((τ ∧ (A ∈ R ∧ B ∈ S ∧ C ∈ D)) → ((AFB) = C ↔ θ))
Theorem	ovres 5603	The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
⊢ ((A ∈ C ∧ B ∈ D) → (A(F ↾ (C × D))B) = (AFB))
Theorem	oprssov 5604	The value of a member of the domain of a subclass of an operation. (Contributed by set.mm contributors, 23-Aug-2007.)
⊢ (((Fun F ∧ G Fn (C × D) ∧ G ⊆ F) ∧ (A ∈ C ∧ B ∈ D)) → (AFB) = (AGB))
Theorem	fovrn 5605	A operations's value belongs to its codomain. (Contributed by set.mm contributors, 27-Aug-2006.)
⊢ ((F:(R × S)–→C ∧ A ∈ R ∧ B ∈ S) → (AFB) ∈ C)
Theorem	fnrnov 5606*	The range of an operation expressed as a collection of the operation's values. (Contributed by set.mm contributors, 29-Oct-2006.)
⊢ (F Fn (A × B) → ran F = {z ∣ ∃x ∈ A ∃y ∈ B z = (xFy)})
Theorem	foov 5607*	An onto mapping of an operation expressed in terms of operation values. (Contributed by set.mm contributors, 29-Oct-2006.)
⊢ (F:(A × B)–onto→C ↔ (F:(A × B)–→C ∧ ∀z ∈ C ∃x ∈ A ∃y ∈ B z = (xFy)))
Theorem	fnovrn 5608	An operation's value belongs to its range. (Contributed by set.mm contributors, 10-Feb-2007.)
⊢ ((F Fn (A × B) ∧ C ∈ A ∧ D ∈ B) → (CFD) ∈ ran F)
Theorem	ovelrn 5609*	A member of an operation's range is a value of the operation. (Contributed by set.mm contributors, 7-Feb-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
⊢ (F Fn (A × B) → (C ∈ ran F ↔ ∃x ∈ A ∃y ∈ B C = (xFy)))
Theorem	funimassov 5610*	Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
⊢ ((Fun F ∧ (A × B) ⊆ dom F) → ((F “ (A × B)) ⊆ C ↔ ∀x ∈ A ∀y ∈ B (xFy) ∈ C))
Theorem	ovelimab 5611*	Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013.)
⊢ ((F Fn A ∧ (B × C) ⊆ A) → (D ∈ (F “ (B × C)) ↔ ∃x ∈ B ∃y ∈ C D = (xFy)))
Theorem	ovconst2 5612	The value of a constant operation. (Contributed by set.mm contributors, 5-Nov-2006.)
⊢ C ∈ V    ⇒   ⊢ ((R ∈ A ∧ S ∈ B) → (R((A × B) × {C})S) = C)
Theorem	oprssdm 5613*	Domain of closure of an operation. (Contributed by set.mm contributors, 24-Aug-1995.)
⊢ ¬ ∅ ∈ S    &   ⊢ ((x ∈ S ∧ y ∈ S) → (xFy) ∈ S)    ⇒   ⊢ (S × S) ⊆ dom F
Theorem	ndmovg 5614	The value of an operation outside its domain. (Contributed by set.mm contributors, 28-Mar-2008.)
⊢ ((dom F = (R × S) ∧ ¬ (A ∈ R ∧ B ∈ S)) → (AFB) = ∅)
Theorem	ndmovcl 5615*	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 is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by set.mm contributors, 24-Sep-2004.)
⊢ dom F = (S × S)    &   ⊢ ((A ∈ S ∧ x ∈ S) → (AFx) ∈ S)    &   ⊢ ∅ ∈ S    ⇒   ⊢ (AFB) ∈ S
Theorem	ndmov 5616	The value of an operation outside its domain. (Contributed by set.mm contributors, 24-Aug-1995.)
⊢ B ∈ V    &   ⊢ dom F = (S × S)    ⇒   ⊢ (¬ (A ∈ S ∧ B ∈ S) → (AFB) = ∅)
Theorem	ndmovrcl 5617	Reverse closure law, when an operation's domain doesn't contain the empty set. (Contributed by set.mm contributors, 3-Feb-1996.)
⊢ B ∈ V    &   ⊢ dom F = (S × S)    &   ⊢ ¬ ∅ ∈ S    ⇒   ⊢ ((AFB) ∈ S → (A ∈ S ∧ B ∈ S))
Theorem	ndmovcom 5618	Any operation is commutative outside its domain. (Contributed by set.mm contributors, 24-Aug-1995.)
⊢ B ∈ V    &   ⊢ dom F = (S × S)    &   ⊢ A ∈ V    ⇒   ⊢ (¬ (A ∈ S ∧ B ∈ S) → (AFB) = (BFA))
Theorem	ndmovass 5619	Any operation is associative outside its domain, if the domain doesn't contain the empty set. (Contributed by set.mm contributors, 24-Aug-1995.)
⊢ B ∈ V    &   ⊢ dom F = (S × S)    &   ⊢ C ∈ V    &   ⊢ ¬ ∅ ∈ S    ⇒   ⊢ (¬ (A ∈ S ∧ B ∈ S ∧ C ∈ S) → ((AFB)FC) = (AF(BFC)))
Theorem	ndmovdistr 5620	Any operation is distributive outside its domain, if the domain doesn't contain the empty set. (Contributed by set.mm contributors, 24-Aug-1995.)
⊢ B ∈ V    &   ⊢ dom F = (S × S)    &   ⊢ C ∈ V    &   ⊢ ¬ ∅ ∈ S    &   ⊢ dom G = (S × S)    ⇒   ⊢ (¬ (A ∈ S ∧ B ∈ S ∧ C ∈ S) → (AG(BFC)) = ((AGB)F(AGC)))
Theorem	ndmovord 5621	Elimination of redundant antecedents in an ordering law. (Contributed by set.mm contributors, 7-Mar-1996.)
⊢ B ∈ V    &   ⊢ dom F = (S × S)    &   ⊢ A ∈ V    &   ⊢ R ⊆ (S × S)    &   ⊢ ¬ ∅ ∈ S    &   ⊢ ((A ∈ S ∧ B ∈ S ∧ C ∈ S) → (ARB ↔ (CFA)R(CFB)))    ⇒   ⊢ (C ∈ S → (ARB ↔ (CFA)R(CFB)))
Theorem	ndmovordi 5622	Elimination of redundant antecedent in an ordering law. (Contributed by set.mm contributors, 25-Jun-1998.)
⊢ A ∈ V    &   ⊢ dom F = (S × S)    &   ⊢ R ⊆ (S × S)    &   ⊢ ¬ ∅ ∈ S    &   ⊢ (C ∈ S → (ARB ↔ (CFA)R(CFB)))    ⇒   ⊢ ((CFA)R(CFB) → ARB)
Theorem	caovcld 5623*	Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.)
⊢ ((φ ∧ (x ∈ C ∧ y ∈ D)) → (xFy) ∈ E)    ⇒   ⊢ ((φ ∧ (A ∈ C ∧ B ∈ D)) → (AFB) ∈ E)
Theorem	caovcl 5624*	Convert an operation closure law to class notation. (Contributed by set.mm contributors, 4-Aug-1995.) (Revised by set.mm contributors, 26-May-2014.)
⊢ ((x ∈ S ∧ y ∈ S) → (xFy) ∈ S)    ⇒   ⊢ ((A ∈ S ∧ B ∈ S) → (AFB) ∈ S)
Theorem	caovcomg 5625*	Convert an operation commutative law to class notation. (Contributed by set.mm contributors, 1-Jun-2013.) (Revised by Mario Carneiro, 2-Jun-2013.)
⊢ ((φ ∧ (x ∈ S ∧ y ∈ S)) → (xFy) = (yFx))    ⇒   ⊢ ((φ ∧ (A ∈ S ∧ B ∈ S)) → (AFB) = (BFA))
Theorem	caovcom 5626*	Convert an operation commutative law to class notation. (Contributed by set.mm contributors, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (xFy) = (yFx)    ⇒   ⊢ (AFB) = (BFA)
Theorem	caovassg 5627*	Convert an operation associative law to class notation. (Contributed by set.mm contributors, 1-Jun-2013.) (Revised by Mario Carneiro, 2-Jun-2013.)
⊢ ((φ ∧ (x ∈ S ∧ y ∈ S ∧ z ∈ S)) → ((xFy)Fz) = (xF(yFz)))    ⇒   ⊢ ((φ ∧ (A ∈ S ∧ B ∈ S ∧ C ∈ S)) → ((AFB)FC) = (AF(BFC)))
Theorem	caovass 5628*	Convert an operation associative law to class notation. (Contributed by set.mm contributors, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ ((xFy)Fz) = (xF(yFz))    ⇒   ⊢ ((AFB)FC) = (AF(BFC))
Theorem	caovcan 5629*	Convert an operation cancellation law to class notation. (Contributed by set.mm contributors, 20-Aug-1995.)
⊢ C ∈ V    &   ⊢ ((x ∈ S ∧ y ∈ S) → ((xFy) = (xFz) → y = z))    ⇒   ⊢ ((A ∈ S ∧ B ∈ S) → ((AFB) = (AFC) → B = C))
Theorem	caovord 5630*	Convert an operation ordering law to class notation. (Contributed by set.mm contributors, 19-Feb-1996.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (z ∈ S → (xRy ↔ (zFx)R(zFy)))    ⇒   ⊢ (C ∈ S → (ARB ↔ (CFA)R(CFB)))
Theorem	caovord2 5631*	Operation ordering law with commuted arguments. (Contributed by set.mm contributors, 27-Feb-1996.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (z ∈ S → (xRy ↔ (zFx)R(zFy)))    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    ⇒   ⊢ (C ∈ S → (ARB ↔ (AFC)R(BFC)))
Theorem	caovord3 5632*	Ordering law. (Contributed by set.mm contributors, 29-Feb-1996.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (z ∈ S → (xRy ↔ (zFx)R(zFy)))    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ D ∈ V    ⇒   ⊢ (((B ∈ S ∧ C ∈ S) ∧ (AFB) = (CFD)) → (ARC ↔ DRB))
Theorem	caovdig 5633*	Convert an operation distributive law to class notation. (Contributed by set.mm contributors, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
⊢ ((φ ∧ (x ∈ S ∧ y ∈ S ∧ z ∈ S)) → (xG(yFz)) = ((xGy)F(xGz)))    ⇒   ⊢ ((φ ∧ (A ∈ S ∧ B ∈ S ∧ C ∈ S)) → (AG(BFC)) = ((AGB)F(AGC)))
Theorem	caovdirg 5634*	Convert an operation reverse distributive law to class notation. (Contributed by set.mm contributors, 19-Oct-2014.)
⊢ ((φ ∧ (x ∈ S ∧ y ∈ S ∧ z ∈ S)) → ((xFy)Gz) = ((xGz)F(yGz)))    ⇒   ⊢ ((φ ∧ (A ∈ S ∧ B ∈ S ∧ C ∈ S)) → ((AFB)GC) = ((AGC)F(BGC)))
Theorem	caovdi 5635*	Convert an operation distributive law to class notation. (Contributed by set.mm contributors, 25-Aug-1995.) (Revised by Mario Carneiro, 28-Jun-2013.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xG(yFz)) = ((xGy)F(xGz))    ⇒   ⊢ (AG(BFC)) = ((AGB)F(AGC))
Theorem	caov32 5636*	Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    ⇒   ⊢ ((AFB)FC) = ((AFC)FB)
Theorem	caov12 5637*	Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    ⇒   ⊢ (AF(BFC)) = (BF(AFC))
Theorem	caov31 5638*	Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    ⇒   ⊢ ((AFB)FC) = ((CFB)FA)
Theorem	caov13 5639*	Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    ⇒   ⊢ (AF(BFC)) = (CF(BFA))
Theorem	caov4 5640*	Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    &   ⊢ D ∈ V    ⇒   ⊢ ((AFB)F(CFD)) = ((AFC)F(BFD))
Theorem	caov411 5641*	Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    &   ⊢ D ∈ V    ⇒   ⊢ ((AFB)F(CFD)) = ((CFB)F(AFD))
Theorem	caov42 5642*	Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    &   ⊢ D ∈ V    ⇒   ⊢ ((AFB)F(CFD)) = ((AFC)F(DFB))
Theorem	caovdir 5643*	Reverse distributive law. (Contributed by set.mm contributors, 26-Aug-1995.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xGy) = (yGx)    &   ⊢ (xG(yFz)) = ((xGy)F(xGz))    ⇒   ⊢ ((AFB)GC) = ((AGC)F(BGC))
Theorem	caovdilem 5644*	Lemma used by real number construction. (Contributed by set.mm contributors, 26-Aug-1995.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xGy) = (yGx)    &   ⊢ (xG(yFz)) = ((xGy)F(xGz))    &   ⊢ D ∈ V    &   ⊢ H ∈ V    &   ⊢ ((xGy)Gz) = (xG(yGz))    ⇒   ⊢ (((AGC)F(BGD))GH) = ((AG(CGH))F(BG(DGH)))
Theorem	caovlem2 5645*	Lemma used in real number construction. (Contributed by set.mm contributors, 26-Aug-1995.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xGy) = (yGx)    &   ⊢ (xG(yFz)) = ((xGy)F(xGz))    &   ⊢ D ∈ V    &   ⊢ H ∈ V    &   ⊢ ((xGy)Gz) = (xG(yGz))    &   ⊢ R ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    ⇒   ⊢ ((((AGC)F(BGD))GH)F(((AGD)F(BGC))GR)) = ((AG((CGH)F(DGR)))F(BG((CGR)F(DGH))))
Theorem	caovmo 5646*	Uniqueness of inverse element in commutative, associative operation with identity. Remark in proof of Proposition 9-2.4 of [Gleason] p. 119. (Contributed by set.mm contributors, 4-Mar-1996.)
⊢ A ∈ V    &   ⊢ B ∈ S    &   ⊢ dom F = (S × S)    &   ⊢ ¬ ∅ ∈ S    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    &   ⊢ (x ∈ S → (xFB) = x)    ⇒   ⊢ ∃*w(AFw) = B
Theorem	oprabid2 5647*	Identity law for operator abstractions. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ {⟨⟨x, y⟩, z⟩ ∣ ⟨⟨x, y⟩, z⟩ ∈ A} = A
Theorem	oprabbi2i 5648*	Biconditional for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ (⟨⟨x, y⟩, z⟩ ∈ A ↔ φ)    ⇒   ⊢ A = {⟨⟨x, y⟩, z⟩ ∣ φ}
Theorem	elovex12 5649	Eliminate antecedent for operator values: domain and range can be taken to be a set. (Contributed by set.mm contributors, 25-Feb-2015.)
⊢ (A ∈ (BFC) → (B ∈ V ∧ C ∈ V))
Theorem	elovex1 5650	Eliminate antecedent for operator values: domain can be taken to be a set. (Contributed by set.mm contributors, 25-Feb-2015.)
⊢ (A ∈ (BFC) → B ∈ V)
Theorem	elovex2 5651	Eliminate antecedent for operator values: range can be taken to be a set. (Contributed by set.mm contributors, 25-Feb-2015.)
⊢ (A ∈ (BFC) → C ∈ V)
2.3.9  "Maps to" notation
Syntax	cmpt 5652	Extend the definition of a class to include maps-to notation for defining a function via a rule.
class (x ∈ A ↦ B)
Definition	df-mpt 5653*	Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from x (in A) to B(x)." The class expression B is the value of the function at x and normally contains the variable x. Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by SF, 5-Jan-2015.)
⊢ (x ∈ A ↦ B) = {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)}
Syntax	cmpt2 5654	Extend the definition of a class to include maps-to notation for defining an operation via a rule.
class (x ∈ A, y ∈ B ↦ C)
Definition	df-mpt2 5655*	Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x, y (in A × B) to B(x, y)." An extension of df-mpt 5653 for two arguments. (Contributed by SF, 5-Jan-2015.)
⊢ (x ∈ A, y ∈ B ↦ C) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = C)}
Theorem	mpteq12f 5656	An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((∀x A = C ∧ ∀x ∈ A B = D) → (x ∈ A ↦ B) = (x ∈ C ↦ D))
Theorem	mpteq12dv 5657*	An equality inference for the maps to notation. (Contributed by set.mm contributors, 24-Aug-2011.) (Revised by set.mm contributors, 16-Dec-2013.)
⊢ (φ → A = C)    &   ⊢ (φ → B = D)    ⇒   ⊢ (φ → (x ∈ A ↦ B) = (x ∈ C ↦ D))
Theorem	mpteq12 5658*	An equality theorem for the maps to notation. (Contributed by set.mm contributors, 16-Dec-2013.)
⊢ ((A = C ∧ ∀x ∈ A B = D) → (x ∈ A ↦ B) = (x ∈ C ↦ D))
Theorem	mpteq1 5659*	An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ (A = B → (x ∈ A ↦ C) = (x ∈ B ↦ C))
Theorem	mpteq2ia 5660	An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ (x ∈ A → B = C)    ⇒   ⊢ (x ∈ A ↦ B) = (x ∈ A ↦ C)
Theorem	mpteq2i 5661	An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ B = C    ⇒   ⊢ (x ∈ A ↦ B) = (x ∈ A ↦ C)
Theorem	mpt2eq123 5662*	An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
⊢ ((A = D ∧ ∀x ∈ A (B = E ∧ ∀y ∈ B C = F)) → (x ∈ A, y ∈ B ↦ C) = (x ∈ D, y ∈ E ↦ F))
Theorem	mpt2eq12 5663*	An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((A = C ∧ B = D) → (x ∈ A, y ∈ B ↦ E) = (x ∈ C, y ∈ D ↦ E))
Theorem	mpt2eq123dv 5664*	An equality deduction for the maps to notation. (Contributed by set.mm contributors, 12-Sep-2011.)
⊢ (φ → A = D)    &   ⊢ (φ → B = E)    &   ⊢ (φ → C = F)    ⇒   ⊢ (φ → (x ∈ A, y ∈ B ↦ C) = (x ∈ D, y ∈ E ↦ F))
Theorem	mpt2eq123i 5665	An equality inference for the maps to notation. (Contributed by set.mm contributors, 15-Jul-2013.)
⊢ A = D    &   ⊢ B = E    &   ⊢ C = F    ⇒   ⊢ (x ∈ A, y ∈ B ↦ C) = (x ∈ D, y ∈ E ↦ F)
Theorem	mpteq12i 5666	An equality inference for the maps to notation. (Contributed by Scott Fenton, 27-Oct-2010.)
⊢ A = C    &   ⊢ B = D    ⇒   ⊢ (x ∈ A ↦ B) = (x ∈ C ↦ D)
Theorem	mpteq2da 5667	Slightly more general equality inference for the maps to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
⊢ Ⅎxφ    &   ⊢ ((φ ∧ x ∈ A) → B = C)    ⇒   ⊢ (φ → (x ∈ A ↦ B) = (x ∈ A ↦ C))
Theorem	mpteq2dva 5668*	Slightly more general equality inference for the maps to notation. (Contributed by Scott Fenton, 25-Apr-2012.)
⊢ ((φ ∧ x ∈ A) → B = C)    ⇒   ⊢ (φ → (x ∈ A ↦ B) = (x ∈ A ↦ C))
Theorem	mpteq2dv 5669*	An equality inference for the maps to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
⊢ (φ → B = C)    ⇒   ⊢ (φ → (x ∈ A ↦ B) = (x ∈ A ↦ C))
Theorem	mpt2eq3dva 5670*	Slightly more general equality inference for the maps to notation. (Contributed by set.mm contributors, 17-Oct-2013.) (Revised by set.mm contributors, 16-Dec-2013.)
⊢ ((φ ∧ x ∈ A ∧ y ∈ B) → C = D)    ⇒   ⊢ (φ → (x ∈ A, y ∈ B ↦ C) = (x ∈ A, y ∈ B ↦ D))
Theorem	mpt2eq3ia 5671	An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((x ∈ A ∧ y ∈ B) → C = D)    ⇒   ⊢ (x ∈ A, y ∈ B ↦ C) = (x ∈ A, y ∈ B ↦ D)
Theorem	nfmpt 5672*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx(y ∈ A ↦ B)
Theorem	nfmpt1 5673	Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
⊢ Ⅎx(x ∈ A ↦ B)
Theorem	nfmpt21 5674	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎx(x ∈ A, y ∈ B ↦ C)
Theorem	nfmpt22 5675	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎy(x ∈ A, y ∈ B ↦ C)
Theorem	nfmpt2 5676*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ ℲzA    &   ⊢ ℲzB    &   ⊢ ℲzC    ⇒   ⊢ Ⅎz(x ∈ A, y ∈ B ↦ C)
Theorem	cbvmpt 5677*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.)
⊢ ℲyB    &   ⊢ ℲxC    &   ⊢ (x = y → B = C)    ⇒   ⊢ (x ∈ A ↦ B) = (y ∈ A ↦ C)
Theorem	cbvmptv 5678*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
⊢ (x = y → B = C)    ⇒   ⊢ (x ∈ A ↦ B) = (y ∈ A ↦ C)
Theorem	cbvmpt2x 5679*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 5680 allows B to be a function of x. (Contributed by NM, 29-Dec-2014.)
⊢ ℲzB    &   ⊢ ℲxD    &   ⊢ ℲzC    &   ⊢ ℲwC    &   ⊢ ℲxE    &   ⊢ ℲyE    &   ⊢ (x = z → B = D)    &   ⊢ ((x = z ∧ y = w) → C = E)    ⇒   ⊢ (x ∈ A, y ∈ B ↦ C) = (z ∈ A, w ∈ D ↦ E)
Theorem	cbvmpt2 5680*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.)
⊢ ℲzC    &   ⊢ ℲwC    &   ⊢ ℲxD    &   ⊢ ℲyD    &   ⊢ ((x = z ∧ y = w) → C = D)    ⇒   ⊢ (x ∈ A, y ∈ B ↦ C) = (z ∈ A, w ∈ B ↦ D)
Theorem	cbvmpt2v 5681*	Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 5677, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)
⊢ (x = z → C = E)    &   ⊢ (y = w → E = D)    ⇒   ⊢ (x ∈ A, y ∈ B ↦ C) = (z ∈ A, w ∈ B ↦ D)
Theorem	fconstmpt 5682*	Representation of a constant function using the mapping operation. (Note that x cannot appear free in B.) (Contributed by set.mm contributors, 16-Nov-2013.)
⊢ (A × {B}) = (x ∈ A ↦ B)
Theorem	mptpreima 5683*	The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ F = (x ∈ A ↦ B)    ⇒   ⊢ (◡F “ C) = {x ∈ A ∣ B ∈ C}
Theorem	dmmpt 5684	The domain of the mapping operation in general. (Contributed by Mario Carneiro, 13-Sep-2013.)
⊢ F = (x ∈ A ↦ B)    ⇒   ⊢ dom F = {x ∈ A ∣ B ∈ V}
Theorem	dmmptg 5685*	The domain of the mapping operation is the stated domain, if the function value is always a set. (Contributed by Mario Carneiro, 9-Feb-2013.)
⊢ (∀x ∈ A B ∈ V → dom (x ∈ A ↦ B) = A)
Theorem	dmmptss 5686*	The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.)
⊢ F = (x ∈ A ↦ B)    ⇒   ⊢ dom F ⊆ A
Theorem	rnmpt 5687*	The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011.)
⊢ F = (x ∈ A ↦ B)    ⇒   ⊢ ran F = {y ∣ ∃x ∈ A y = B}
Theorem	funmpt 5688	A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ Fun (x ∈ A ↦ B)
Theorem	mptfng 5689*	The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011.)
⊢ F = (x ∈ A ↦ B)    ⇒   ⊢ (∀x ∈ A B ∈ V ↔ F Fn A)
Theorem	fnmpt 5690*	The maps-to notation defines a function with domain. (Contributed by set.mm contributors, 9-Apr-2013.)
⊢ F = (x ∈ A ↦ B)    ⇒   ⊢ (∀x ∈ A B ∈ V → F Fn A)
Theorem	fnmpti 5691*	Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ B ∈ V    &   ⊢ F = (x ∈ A ↦ B)    ⇒   ⊢ F Fn A
Theorem	dmmpti 5692*	Domain of an ordered-pair class abstraction that specifies a function. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ B ∈ V    &   ⊢ F = (x ∈ A ↦ B)    ⇒   ⊢ dom F = A
Theorem	fmpt 5693*	Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ F = (x ∈ A ↦ C)    ⇒   ⊢ (∀x ∈ A C ∈ B ↔ F:A–→B)
Theorem	fmpti 5694*	Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ F = (x ∈ A ↦ C)    &   ⊢ (x ∈ A → C ∈ B)    ⇒   ⊢ F:A–→B
Theorem	fmptd 5695*	Domain and co-domain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ ((φ ∧ x ∈ A) → B ∈ C)    &   ⊢ F = (x ∈ A ↦ B)    ⇒   ⊢ (φ → F:A–→C)
Theorem	fmpt2d 5696*	Domain and co-domain of the mapping operation; deduction form. (Contributed by set.mm contributors, 9-Apr-2013.)
⊢ (φ → (x ∈ A → B ∈ V))    &   ⊢ F = (x ∈ A ↦ B)    &   ⊢ (φ → (y ∈ A → (F ‘y) ∈ C))    ⇒   ⊢ (φ → F:A–→C)
Theorem	resmpt 5697*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.)
⊢ (B ⊆ A → ((x ∈ A ↦ C) ↾ B) = (x ∈ B ↦ C))
Theorem	resmpt2 5698*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)
⊢ ((C ⊆ A ∧ D ⊆ B) → ((x ∈ A, y ∈ B ↦ E) ↾ (C × D)) = (x ∈ C, y ∈ D ↦ E))
Theorem	fvmptg 5699*	Value of a function given in maps-to notation. Analogous to fvopab4g 5389. (Contributed by set.mm contributors, 2-Oct-2007.) (Revised by set.mm contributors, 4-Aug-2008.)
⊢ (x = A → B = C)    &   ⊢ F = (x ∈ D ↦ B)    ⇒   ⊢ ((A ∈ D ∧ C ∈ R) → (F ‘A) = C)
Theorem	fvmpti 5700*	Value of a function given in maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ (x = A → B = C)    &   ⊢ F = (x ∈ D ↦ B)    ⇒   ⊢ (A ∈ D → (F ‘A) = ( I ‘C))