P. 49 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4801-4900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ressn 4801	Restriction of a class to a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ (A ↾ {B}) = ({B} × (A “ {B}))
Theorem	cnviinm 4802*	The converse of an intersection is the intersection of the converse. (Contributed by Jim Kingdon, 18-Dec-2018.)
⊢ (∃y y ∈ A → ◡∩ x ∈ A B = ∩ x ∈ A ◡B)
Theorem	cnvpom 4803*	The converse of a partial order relation is a partial order relation. (Contributed by NM, 15-Jun-2005.)
⊢ (∃x x ∈ A → (𝑅 Po A ↔ ◡𝑅 Po A))
Theorem	cnvsom 4804*	The converse of a strict order relation is a strict order relation. (Contributed by Jim Kingdon, 19-Dec-2018.)
⊢ (∃x x ∈ A → (𝑅 Or A ↔ ◡𝑅 Or A))
Theorem	coexg 4805	The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (A ∘ B) ∈ V)
Theorem	coex 4806	The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A ∘ B) ∈ V
Theorem	xpcom 4807*	Composition of two cross products. (Contributed by Jim Kingdon, 20-Dec-2018.)
⊢ (∃x x ∈ B → ((B × 𝐶) ∘ (A × B)) = (A × 𝐶))
2.6.7  Definite description binder (inverted iota)
Syntax	cio 4808	Extend class notation with Russell's definition description binder (inverted iota).
class (℩xφ)
Theorem	iotajust 4809*	Soundness justification theorem for df-iota 4810. (Contributed by Andrew Salmon, 29-Jun-2011.)
⊢ ∪ {y ∣ {x ∣ φ} = {y}} = ∪ {z ∣ {x ∣ φ} = {z}}
Definition	df-iota 4810*	Define Russell's definition description binder, which can be read as "the unique x such that φ," where φ ordinarily contains x as a free variable. Our definition is meaningful only when there is exactly one x such that φ is true (see iotaval 4821); otherwise, it evaluates to the empty set (see iotanul 4825). Russell used the inverted iota symbol ℩ to represent the binder. Sometimes proofs need to expand an iota-based definition. That is, given "X = the x for which ... x ... x ..." holds, the proof needs to get to "... X ... X ...". A general strategy to do this is to use iotacl 4833 (for unbounded iota). This can be easier than applying a version that applies an explicit substitution, because substituting an iota into its own property always has a bound variable clash which must be first renamed or else guarded with NF. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (℩xφ) = ∪ {y ∣ {x ∣ φ} = {y}}
Theorem	dfiota2 4811*	Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (℩xφ) = ∪ {y ∣ ∀x(φ ↔ x = y)}
Theorem	nfiota1 4812	Bound-variable hypothesis builder for the ℩ class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎx(℩xφ)
Theorem	nfiotadxy 4813*	Deduction version of nfiotaxy 4814. (Contributed by Jim Kingdon, 21-Dec-2018.)
⊢ Ⅎyφ    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx(℩yψ))
Theorem	nfiotaxy 4814*	Bound-variable hypothesis builder for the ℩ class. (Contributed by NM, 23-Aug-2011.)
⊢ Ⅎxφ    ⇒   ⊢ Ⅎx(℩yφ)
Theorem	cbviota 4815	Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
⊢ (x = y → (φ ↔ ψ))    &   ⊢ Ⅎyφ    &   ⊢ Ⅎxψ    ⇒   ⊢ (℩xφ) = (℩yψ)
Theorem	cbviotav 4816*	Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (℩xφ) = (℩yψ)
Theorem	sb8iota 4817	Variable substitution in description binder. Compare sb8eu 1910. (Contributed by NM, 18-Mar-2013.)
⊢ Ⅎyφ    ⇒   ⊢ (℩xφ) = (℩y[y / x]φ)
Theorem	iotaeq 4818	Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (∀x x = y → (℩xφ) = (℩yφ))
Theorem	iotabi 4819	Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (∀x(φ ↔ ψ) → (℩xφ) = (℩xψ))
Theorem	uniabio 4820*	Part of Theorem 8.17 in [Quine] p. 56. This theorem serves as a lemma for the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∀x(φ ↔ x = y) → ∪ {x ∣ φ} = y)
Theorem	iotaval 4821*	Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∀x(φ ↔ x = y) → (℩xφ) = y)
Theorem	iotauni 4822	Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!xφ → (℩xφ) = ∪ {x ∣ φ})
Theorem	iotaint 4823	Equivalence between two different forms of ℩. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (∃!xφ → (℩xφ) = ∩ {x ∣ φ})
Theorem	iota1 4824	Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!xφ → (φ ↔ (℩xφ) = x))
Theorem	iotanul 4825	Theorem 8.22 in [Quine] p. 57. This theorem is the result if there isn't exactly one x that satisfies φ. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (¬ ∃!xφ → (℩xφ) = ∅)
Theorem	euiotaex 4826	Theorem 8.23 in [Quine] p. 58, with existential uniqueness condition added. This theorem proves the existence of the ℩ class under our definition. (Contributed by Jim Kingdon, 21-Dec-2018.)
⊢ (∃!xφ → (℩xφ) ∈ V)
Theorem	iotass 4827*	Value of iota based on a proposition which holds only for values which are subsets of a given class. (Contributed by Mario Carneiro and Jim Kingdon, 21-Dec-2018.)
⊢ (∀x(φ → x ⊆ A) → (℩xφ) ⊆ A)
Theorem	iota4 4828	Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!xφ → [(℩xφ) / x]φ)
Theorem	iota4an 4829	Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!x(φ ∧ ψ) → [(℩x(φ ∧ ψ)) / x]φ)
Theorem	iota5 4830*	A method for computing iota. (Contributed by NM, 17-Sep-2013.)
⊢ ((φ ∧ A ∈ 𝑉) → (ψ ↔ x = A))    ⇒   ⊢ ((φ ∧ A ∈ 𝑉) → (℩xψ) = A)
Theorem	iotabidv 4831*	Formula-building deduction rule for iota. (Contributed by NM, 20-Aug-2011.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (℩xψ) = (℩xχ))
Theorem	iotabii 4832	Formula-building deduction rule for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (℩xφ) = (℩xψ)
Theorem	iotacl 4833	Membership law for descriptions. This can useful for expanding an unbounded iota-based definition (see df-iota 4810). (Contributed by Andrew Salmon, 1-Aug-2011.)
⊢ (∃!xφ → (℩xφ) ∈ {x ∣ φ})
Theorem	iota2df 4834	A condition that allows us to represent "the unique element such that φ " with a class expression A. (Contributed by NM, 30-Dec-2014.)
⊢ (φ → B ∈ 𝑉)    &   ⊢ (φ → ∃!xψ)    &   ⊢ ((φ ∧ x = B) → (ψ ↔ χ))    &   ⊢ Ⅎxφ    &   ⊢ (φ → Ⅎxχ)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → (χ ↔ (℩xψ) = B))
Theorem	iota2d 4835*	A condition that allows us to represent "the unique element such that φ " with a class expression A. (Contributed by NM, 30-Dec-2014.)
⊢ (φ → B ∈ 𝑉)    &   ⊢ (φ → ∃!xψ)    &   ⊢ ((φ ∧ x = B) → (ψ ↔ χ))    ⇒   ⊢ (φ → (χ ↔ (℩xψ) = B))
Theorem	iota2 4836*	The unique element such that φ. (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ B ∧ ∃!xφ) → (ψ ↔ (℩xφ) = A))
Theorem	sniota 4837	A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!xφ → {x ∣ φ} = {(℩xφ)})
Theorem	csbiotag 4838*	Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.)
⊢ (A ∈ 𝑉 → ⦋A / x⦌(℩yφ) = (℩y[A / x]φ))
2.6.8  Functions
Syntax	wfun 4839	Extend the definition of a wff to include the function predicate. (Read: A is a function.)
wff Fun A
Syntax	wfn 4840	Extend the definition of a wff to include the function predicate with a domain. (Read: A is a function on B.)
wff A Fn B
Syntax	wf 4841	Extend the definition of a wff to include the function predicate with domain and codomain. (Read: 𝐹 maps A into B.)
wff 𝐹:A⟶B
Syntax	wf1 4842	Extend the definition of a wff to include one-to-one functions. (Read: 𝐹 maps A one-to-one into B.) The notation ("1-1" above the arrow) is from Definition 6.15(5) of [TakeutiZaring] p. 27.
wff 𝐹:A–1-1→B
Syntax	wfo 4843	Extend the definition of a wff to include onto functions. (Read: 𝐹 maps A onto B.) The notation ("onto" below the arrow) is from Definition 6.15(4) of [TakeutiZaring] p. 27.
wff 𝐹:A–onto→B
Syntax	wf1o 4844	Extend the definition of a wff to include one-to-one onto functions. (Read: 𝐹 maps A one-to-one onto B.) The notation ("1-1" above the arrow and "onto" below the arrow) is from Definition 6.15(6) of [TakeutiZaring] p. 27.
wff 𝐹:A–1-1-onto→B
Syntax	cfv 4845	Extend the definition of a class to include the value of a function. (Read: The value of 𝐹 at A, or "𝐹 of A.")
class (𝐹‘A)
Syntax	wiso 4846	Extend the definition of a wff to include the isomorphism property. (Read: 𝐻 is an 𝑅, 𝑆 isomorphism of A onto B.)
wff 𝐻 Isom 𝑅, 𝑆 (A, B)
Definition	df-fun 4847	Define predicate that determines if some class A is a function. Definition 10.1 of [Quine] p. 65. For example, the expression Fun I is true (funi 4875). This is not the same as defining a specific function's mapping, which is typically done using the format of cmpt 3809 with the maps-to notation (see df-mpt 3811). Contrast this predicate with the predicates to determine if some class is a function with a given domain (df-fn 4848), a function with a given domain and codomain (df-f 4849), a one-to-one function (df-f1 4850), an onto function (df-fo 4851), or a one-to-one onto function (df-f1o 4852). For alternate definitions, see dffun2 4855, dffun4 4856, dffun6 4859, dffun7 4871, dffun8 4872, and dffun9 4873. (Contributed by NM, 1-Aug-1994.)
⊢ (Fun A ↔ (Rel A ∧ (A ∘ ◡A) ⊆ I ))
Definition	df-fn 4848	Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.)
⊢ (A Fn B ↔ (Fun A ∧ dom A = B))
Definition	df-f 4849	Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:A⟶B ↔ (𝐹 Fn A ∧ ran 𝐹 ⊆ B))
Definition	df-f1 4850	Define a one-to-one function. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:A–1-1→B ↔ (𝐹:A⟶B ∧ Fun ◡𝐹))
Definition	df-fo 4851	Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:A–onto→B ↔ (𝐹 Fn A ∧ ran 𝐹 = B))
Definition	df-f1o 4852	Define a one-to-one onto function. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:A–1-1-onto→B ↔ (𝐹:A–1-1→B ∧ 𝐹:A–onto→B))
Definition	df-fv 4853*	Define the value of a function, (𝐹‘A), also known as function application. For example, ( I ‘∅) = ∅. Typically, function 𝐹 is defined using maps-to notation (see df-mpt 3811), but this is not required. For example, F = { ⟨ 2 , 6 ⟩, ⟨ 3 , 9 ⟩ } -> ( F ‘ 3 ) = 9 . We will later define two-argument functions using ordered pairs as (A𝐹B) = (𝐹‘⟨A, B⟩). This particular definition is quite convenient: it can be applied to any class and evaluates to the empty set when it is not meaningful. The left apostrophe notation originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell] p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26. It means the same thing as the more familiar 𝐹(A) notation for a function's value at A, i.e. "𝐹 of A," but without context-dependent notational ambiguity. (Contributed by NM, 1-Aug-1994.) Revised to use ℩. (Revised by Scott Fenton, 6-Oct-2017.)
⊢ (𝐹‘A) = (℩xA𝐹x)
Definition	df-isom 4854*	Define the isomorphism predicate. We read this as "𝐻 is an 𝑅, 𝑆 isomorphism of A onto B." Normally, 𝑅 and 𝑆 are ordering relations on A and B respectively. Definition 6.28 of [TakeutiZaring] p. 32, whose notation is the same as ours except that 𝑅 and 𝑆 are subscripts. (Contributed by NM, 4-Mar-1997.)
⊢ (𝐻 Isom 𝑅, 𝑆 (A, B) ↔ (𝐻:A–1-1-onto→B ∧ ∀x ∈ A ∀y ∈ A (x𝑅y ↔ (𝐻‘x)𝑆(𝐻‘y))))
Theorem	dffun2 4855*	Alternate definition of a function. (Contributed by NM, 29-Dec-1996.)
⊢ (Fun A ↔ (Rel A ∧ ∀x∀y∀z((xAy ∧ xAz) → y = z)))
Theorem	dffun4 4856*	Alternate definition of a function. Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 29-Dec-1996.)
⊢ (Fun A ↔ (Rel A ∧ ∀x∀y∀z((⟨x, y⟩ ∈ A ∧ ⟨x, z⟩ ∈ A) → y = z)))
Theorem	dffun5r 4857*	A way of proving a relation is a function, analogous to mo2r 1949. (Contributed by Jim Kingdon, 27-May-2020.)
⊢ ((Rel A ∧ ∀x∃z∀y(⟨x, y⟩ ∈ A → y = z)) → Fun A)
Theorem	dffun6f 4858*	Definition of function, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲyA    ⇒   ⊢ (Fun A ↔ (Rel A ∧ ∀x∃*y xAy))
Theorem	dffun6 4859*	Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.)
⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀x∃*y x𝐹y))
Theorem	funmo 4860*	A function has at most one value for each argument. (Contributed by NM, 24-May-1998.)
⊢ (Fun 𝐹 → ∃*y A𝐹y)
Theorem	dffun4f 4861*	Definition of function like dffun4 4856 but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Jim Kingdon, 17-Mar-2019.)
⊢ ℲxA    &   ⊢ ℲyA    &   ⊢ ℲzA    ⇒   ⊢ (Fun A ↔ (Rel A ∧ ∀x∀y∀z((⟨x, y⟩ ∈ A ∧ ⟨x, z⟩ ∈ A) → y = z)))
Theorem	funrel 4862	A function is a relation. (Contributed by NM, 1-Aug-1994.)
⊢ (Fun A → Rel A)
Theorem	funss 4863	Subclass theorem for function predicate. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.)
⊢ (A ⊆ B → (Fun B → Fun A))
Theorem	funeq 4864	Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.)
⊢ (A = B → (Fun A ↔ Fun B))
Theorem	funeqi 4865	Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ A = B    ⇒   ⊢ (Fun A ↔ Fun B)
Theorem	funeqd 4866	Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (Fun A ↔ Fun B))
Theorem	nffun 4867	Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004.)
⊢ Ⅎx𝐹    ⇒   ⊢ ℲxFun 𝐹
Theorem	sbcfung 4868	Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
⊢ (A ∈ 𝑉 → ([A / x]Fun 𝐹 ↔ Fun ⦋A / x⦌𝐹))
Theorem	funeu 4869*	There is exactly one value of a function. (Contributed by NM, 22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((Fun 𝐹 ∧ A𝐹B) → ∃!y A𝐹y)
Theorem	funeu2 4870*	There is exactly one value of a function. (Contributed by NM, 3-Aug-1994.)
⊢ ((Fun 𝐹 ∧ ⟨A, B⟩ ∈ 𝐹) → ∃!y⟨A, y⟩ ∈ 𝐹)
Theorem	dffun7 4871*	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. (Enderton's definition is ambiguous because "there is only one" could mean either "there is at most one" or "there is exactly one." However, dffun8 4872 shows that it doesn't matter which meaning we pick.) (Contributed by NM, 4-Nov-2002.)
⊢ (Fun A ↔ (Rel A ∧ ∀x ∈ dom A∃*y xAy))
Theorem	dffun8 4872*	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 4871. (Contributed by NM, 4-Nov-2002.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (Fun A ↔ (Rel A ∧ ∀x ∈ dom A∃!y xAy))
Theorem	dffun9 4873*	Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.)
⊢ (Fun A ↔ (Rel A ∧ ∀x ∈ dom A∃*y ∈ ran A xAy))
Theorem	funfn 4874	An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)
⊢ (Fun A ↔ A Fn dom A)
Theorem	funi 4875	The identity relation is a function. Part of Theorem 10.4 of [Quine] p. 65. (Contributed by NM, 30-Apr-1998.)
⊢ Fun I
Theorem	nfunv 4876	The universe is not a function. (Contributed by Raph Levien, 27-Jan-2004.)
⊢ ¬ Fun V
Theorem	funopg 4877	A Kuratowski ordered pair is a function only if its components are equal. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ Fun ⟨A, B⟩) → A = B)
Theorem	funopab 4878*	A class of ordered pairs is a function when there is at most one second member for each pair. (Contributed by NM, 16-May-1995.)
⊢ (Fun {⟨x, y⟩ ∣ φ} ↔ ∀x∃*yφ)
Theorem	funopabeq 4879*	A class of ordered pairs of values is a function. (Contributed by NM, 14-Nov-1995.)
⊢ Fun {⟨x, y⟩ ∣ y = A}
Theorem	funopab4 4880*	A class of ordered pairs of values in the form used by df-mpt 3811 is a function. (Contributed by NM, 17-Feb-2013.)
⊢ Fun {⟨x, y⟩ ∣ (φ ∧ y = A)}
Theorem	funmpt 4881	A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ Fun (x ∈ A ↦ B)
Theorem	funmpt2 4882	Functionality of a class given by a "maps to" notation. (Contributed by FL, 17-Feb-2008.) (Revised by Mario Carneiro, 31-May-2014.)
⊢ 𝐹 = (x ∈ A ↦ B)    ⇒   ⊢ Fun 𝐹
Theorem	funco 4883	The composition of two functions is a function. Exercise 29 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Fun (𝐹 ∘ 𝐺))
Theorem	funres 4884	A restriction of a function is a function. Compare Exercise 18 of [TakeutiZaring] p. 25. (Contributed by NM, 16-Aug-1994.)
⊢ (Fun 𝐹 → Fun (𝐹 ↾ A))
Theorem	funssres 4885	The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994.)
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹) → (𝐹 ↾ dom 𝐺) = 𝐺)
Theorem	fun2ssres 4886	Equality of restrictions of a function and a subclass. (Contributed by NM, 16-Aug-1994.)
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ A ⊆ dom 𝐺) → (𝐹 ↾ A) = (𝐺 ↾ A))
Theorem	funun 4887	The union of functions with disjoint domains is a function. Theorem 4.6 of [Monk1] p. 43. (Contributed by NM, 12-Aug-1994.)
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹 ∪ 𝐺))
Theorem	funcnvsn 4888	The converse singleton of an ordered pair is a function. This is equivalent to funsn 4891 via cnvsn 4746, but stating it this way allows us to skip the sethood assumptions on A and B. (Contributed by NM, 30-Apr-2015.)
⊢ Fun ◡{⟨A, B⟩}
Theorem	funsng 4889	A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 28-Jun-2011.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → Fun {⟨A, B⟩})
Theorem	fnsng 4890	Functionality and domain of the singleton of an ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → {⟨A, B⟩} Fn {A})
Theorem	funsn 4891	A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 12-Aug-1994.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ Fun {⟨A, B⟩}
Theorem	funprg 4892	A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011.)
⊢ (((A ∈ 𝑉 ∧ B ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ A ≠ B) → Fun {⟨A, 𝐶⟩, ⟨B, 𝐷⟩})
Theorem	funtpg 4893	A set of three pairs is a function if their first members are different. (Contributed by Alexander van der Vekens, 5-Dec-2017.)
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (A ∈ 𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {⟨𝑋, A⟩, ⟨𝑌, B⟩, ⟨𝑍, 𝐶⟩})
Theorem	funpr 4894	A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (A ≠ B → Fun {⟨A, 𝐶⟩, ⟨B, 𝐷⟩})
Theorem	funtp 4895	A function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ ((A ≠ B ∧ A ≠ 𝐶 ∧ B ≠ 𝐶) → Fun {⟨A, 𝐷⟩, ⟨B, 𝐸⟩, ⟨𝐶, 𝐹⟩})
Theorem	fnsn 4896	Functionality and domain of the singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ {⟨A, B⟩} Fn {A}
Theorem	fnprg 4897	Function with a domain of two different values. (Contributed by FL, 26-Jun-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (((A ∈ 𝑉 ∧ B ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ A ≠ B) → {⟨A, 𝐶⟩, ⟨B, 𝐷⟩} Fn {A, B})
Theorem	fntpg 4898	Function with a domain of three different values. (Contributed by Alexander van der Vekens, 5-Dec-2017.)
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (A ∈ 𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {⟨𝑋, A⟩, ⟨𝑌, B⟩, ⟨𝑍, 𝐶⟩} Fn {𝑋, 𝑌, 𝑍})
Theorem	fntp 4899	A function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ ((A ≠ B ∧ A ≠ 𝐶 ∧ B ≠ 𝐶) → {⟨A, 𝐷⟩, ⟨B, 𝐸⟩, ⟨𝐶, 𝐹⟩} Fn {A, B, 𝐶})
Theorem	fun0 4900	The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed by NM, 7-Apr-1998.)
⊢ Fun ∅