Theorem List for Intuitionistic Logic Explorer - 5101-5200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | funssres 5101 |
The restriction of a function to the domain of a subclass equals the
subclass. (Contributed by NM, 15-Aug-1994.)
|
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹) → (𝐹 ↾ dom 𝐺) = 𝐺) |
|
Theorem | fun2ssres 5102 |
Equality of restrictions of a function and a subclass. (Contributed by
NM, 16-Aug-1994.)
|
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ⊆ dom 𝐺) → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴)) |
|
Theorem | funun 5103 |
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 5104 |
The converse singleton of an ordered pair is a function. This is
equivalent to funsn 5107 via cnvsn 4957, but stating it this way allows us to
skip the sethood assumptions on 𝐴 and 𝐵. (Contributed by NM,
30-Apr-2015.)
|
⊢ Fun ◡{〈𝐴, 𝐵〉} |
|
Theorem | funsng 5105 |
A singleton of an ordered pair is a function. Theorem 10.5 of [Quine]
p. 65. (Contributed by NM, 28-Jun-2011.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Fun {〈𝐴, 𝐵〉}) |
|
Theorem | fnsng 5106 |
Functionality and domain of the singleton of an ordered pair.
(Contributed by Mario Carneiro, 30-Apr-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {〈𝐴, 𝐵〉} Fn {𝐴}) |
|
Theorem | funsn 5107 |
A singleton of an ordered pair is a function. Theorem 10.5 of [Quine]
p. 65. (Contributed by NM, 12-Aug-1994.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ Fun {〈𝐴, 𝐵〉} |
|
Theorem | funinsn 5108 |
A function based on the singleton of an ordered pair. Unlike funsng 5105,
this holds even if 𝐴 or 𝐵 is a proper class.
(Contributed by
Jim Kingdon, 17-Apr-2022.)
|
⊢ Fun ({〈𝐴, 𝐵〉} ∩ (𝑉 × 𝑊)) |
|
Theorem | funprg 5109 |
A set of two pairs is a function if their first members are different.
(Contributed by FL, 26-Jun-2011.)
|
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → Fun {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}) |
|
Theorem | funtpg 5110 |
A set of three pairs is a function if their first members are different.
(Contributed by Alexander van der Vekens, 5-Dec-2017.)
|
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉}) |
|
Theorem | funpr 5111 |
A function with a domain of two elements. (Contributed by Jeff Madsen,
20-Jun-2010.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ (𝐴 ≠ 𝐵 → Fun {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}) |
|
Theorem | funtp 5112 |
A function with a domain of three elements. (Contributed by NM,
14-Sep-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈
V ⇒ ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → Fun {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}) |
|
Theorem | fnsn 5113 |
Functionality and domain of the singleton of an ordered pair.
(Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ {〈𝐴, 𝐵〉} Fn {𝐴} |
|
Theorem | fnprg 5114 |
Function with a domain of two different values. (Contributed by FL,
26-Jun-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} Fn {𝐴, 𝐵}) |
|
Theorem | fntpg 5115 |
Function with a domain of three different values. (Contributed by
Alexander van der Vekens, 5-Dec-2017.)
|
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} Fn {𝑋, 𝑌, 𝑍}) |
|
Theorem | fntp 5116 |
A function with a domain of three elements. (Contributed by NM,
14-Sep-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈
V ⇒ ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉} Fn {𝐴, 𝐵, 𝐶}) |
|
Theorem | fun0 5117 |
The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed
by NM, 7-Apr-1998.)
|
⊢ Fun ∅ |
|
Theorem | funcnvcnv 5118 |
The double converse of a function is a function. (Contributed by NM,
21-Sep-2004.)
|
⊢ (Fun 𝐴 → Fun ◡◡𝐴) |
|
Theorem | funcnv2 5119* |
A simpler equivalence for single-rooted (see funcnv 5120). (Contributed
by NM, 9-Aug-2004.)
|
⊢ (Fun ◡𝐴 ↔ ∀𝑦∃*𝑥 𝑥𝐴𝑦) |
|
Theorem | funcnv 5120* |
The converse of a class is a function iff the class is single-rooted,
which means that for any 𝑦 in the range of 𝐴 there
is at most
one 𝑥 such that 𝑥𝐴𝑦. Definition of single-rooted in
[Enderton] p. 43. See funcnv2 5119 for a simpler version. (Contributed by
NM, 13-Aug-2004.)
|
⊢ (Fun ◡𝐴 ↔ ∀𝑦 ∈ ran 𝐴∃*𝑥 𝑥𝐴𝑦) |
|
Theorem | funcnv3 5121* |
A condition showing a class is single-rooted. (See funcnv 5120).
(Contributed by NM, 26-May-2006.)
|
⊢ (Fun ◡𝐴 ↔ ∀𝑦 ∈ ran 𝐴∃!𝑥 ∈ dom 𝐴 𝑥𝐴𝑦) |
|
Theorem | funcnveq 5122* |
Another way of expressing that a class is single-rooted. Counterpart to
dffun2 5069. (Contributed by Jim Kingdon, 24-Dec-2018.)
|
⊢ (Fun ◡𝐴 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑦) → 𝑥 = 𝑧)) |
|
Theorem | fun2cnv 5123* |
The double converse of a class is a function iff the class is
single-valued. Each side is equivalent to Definition 6.4(2) of
[TakeutiZaring] p. 23, who use the
notation "Un(A)" for single-valued.
Note that 𝐴 is not necessarily a function.
(Contributed by NM,
13-Aug-2004.)
|
⊢ (Fun ◡◡𝐴 ↔ ∀𝑥∃*𝑦 𝑥𝐴𝑦) |
|
Theorem | svrelfun 5124 |
A single-valued relation is a function. (See fun2cnv 5123 for
"single-valued.") Definition 6.4(4) of [TakeutiZaring] p. 24.
(Contributed by NM, 17-Jan-2006.)
|
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ Fun ◡◡𝐴)) |
|
Theorem | fncnv 5125* |
Single-rootedness (see funcnv 5120) of a class cut down by a cross
product. (Contributed by NM, 5-Mar-2007.)
|
⊢ (◡(𝑅 ∩ (𝐴 × 𝐵)) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑥𝑅𝑦) |
|
Theorem | fun11 5126* |
Two ways of stating that 𝐴 is one-to-one (but not necessarily a
function). Each side is equivalent to Definition 6.4(3) of
[TakeutiZaring] p. 24, who use the
notation "Un2 (A)" for one-to-one
(but not necessarily a function). (Contributed by NM, 17-Jan-2006.)
|
⊢ ((Fun ◡◡𝐴 ∧ Fun ◡𝐴) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤))) |
|
Theorem | fununi 5127* |
The union of a chain (with respect to inclusion) of functions is a
function. (Contributed by NM, 10-Aug-2004.)
|
⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪
𝐴) |
|
Theorem | funcnvuni 5128* |
The union of a chain (with respect to inclusion) of single-rooted sets
is single-rooted. (See funcnv 5120 for "single-rooted"
definition.)
(Contributed by NM, 11-Aug-2004.)
|
⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴) |
|
Theorem | fun11uni 5129* |
The union of a chain (with respect to inclusion) of one-to-one functions
is a one-to-one function. (Contributed by NM, 11-Aug-2004.)
|
⊢ (∀𝑓 ∈ 𝐴 ((Fun 𝑓 ∧ Fun ◡𝑓) ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (Fun ∪
𝐴 ∧ Fun ◡∪ 𝐴)) |
|
Theorem | funin 5130 |
The intersection with a function is a function. Exercise 14(a) of
[Enderton] p. 53. (Contributed by NM,
19-Mar-2004.) (Proof shortened by
Andrew Salmon, 17-Sep-2011.)
|
⊢ (Fun 𝐹 → Fun (𝐹 ∩ 𝐺)) |
|
Theorem | funres11 5131 |
The restriction of a one-to-one function is one-to-one. (Contributed by
NM, 25-Mar-1998.)
|
⊢ (Fun ◡𝐹 → Fun ◡(𝐹 ↾ 𝐴)) |
|
Theorem | funcnvres 5132 |
The converse of a restricted function. (Contributed by NM,
27-Mar-1998.)
|
⊢ (Fun ◡𝐹 → ◡(𝐹 ↾ 𝐴) = (◡𝐹 ↾ (𝐹 “ 𝐴))) |
|
Theorem | cnvresid 5133 |
Converse of a restricted identity function. (Contributed by FL,
4-Mar-2007.)
|
⊢ ◡( I
↾ 𝐴) = ( I ↾
𝐴) |
|
Theorem | funcnvres2 5134 |
The converse of a restriction of the converse of a function equals the
function restricted to the image of its converse. (Contributed by NM,
4-May-2005.)
|
⊢ (Fun 𝐹 → ◡(◡𝐹 ↾ 𝐴) = (𝐹 ↾ (◡𝐹 “ 𝐴))) |
|
Theorem | funimacnv 5135 |
The image of the preimage of a function. (Contributed by NM,
25-May-2004.)
|
⊢ (Fun 𝐹 → (𝐹 “ (◡𝐹 “ 𝐴)) = (𝐴 ∩ ran 𝐹)) |
|
Theorem | funimass1 5136 |
A kind of contraposition law that infers a subclass of an image from a
preimage subclass. (Contributed by NM, 25-May-2004.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹) → ((◡𝐹 “ 𝐴) ⊆ 𝐵 → 𝐴 ⊆ (𝐹 “ 𝐵))) |
|
Theorem | funimass2 5137 |
A kind of contraposition law that infers an image subclass from a subclass
of a preimage. (Contributed by NM, 25-May-2004.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ (◡𝐹 “ 𝐵)) → (𝐹 “ 𝐴) ⊆ 𝐵) |
|
Theorem | imadiflem 5138 |
One direction of imadif 5139. This direction does not require
Fun ◡𝐹. (Contributed by Jim
Kingdon, 25-Dec-2018.)
|
⊢ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)) ⊆ (𝐹 “ (𝐴 ∖ 𝐵)) |
|
Theorem | imadif 5139 |
The image of a difference is the difference of images. (Contributed by
NM, 24-May-1998.)
|
⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))) |
|
Theorem | imainlem 5140 |
One direction of imain 5141. This direction does not require
Fun ◡𝐹. (Contributed by Jim
Kingdon, 25-Dec-2018.)
|
⊢ (𝐹 “ (𝐴 ∩ 𝐵)) ⊆ ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)) |
|
Theorem | imain 5141 |
The image of an intersection is the intersection of images.
(Contributed by Paul Chapman, 11-Apr-2009.)
|
⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∩ 𝐵)) = ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵))) |
|
Theorem | funimaexglem 5142 |
Lemma for funimaexg 5143. It constitutes the interesting part of
funimaexg 5143, in which 𝐵 ⊆ dom 𝐴. (Contributed by Jim Kingdon,
27-Dec-2018.)
|
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ dom 𝐴) → (𝐴 “ 𝐵) ∈ V) |
|
Theorem | funimaexg 5143 |
Axiom of Replacement using abbreviations. Axiom 39(vi) of [Quine] p. 284.
Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM,
10-Sep-2006.)
|
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 “ 𝐵) ∈ V) |
|
Theorem | funimaex 5144 |
The image of a set under any function is also a set. Equivalent of
Axiom of Replacement. Axiom 39(vi) of [Quine] p. 284. Compare Exercise
9 of [TakeutiZaring] p. 29.
(Contributed by NM, 17-Nov-2002.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (Fun 𝐴 → (𝐴 “ 𝐵) ∈ V) |
|
Theorem | isarep1 5145* |
Part of a study of the Axiom of Replacement used by the Isabelle prover.
The object PrimReplace is apparently the image of the function encoded
by 𝜑(𝑥, 𝑦) i.e. the class ({〈𝑥, 𝑦〉 ∣ 𝜑} “ 𝐴).
If so, we can prove Isabelle's "Axiom of Replacement"
conclusion without
using the Axiom of Replacement, for which I (N. Megill) currently have
no explanation. (Contributed by NM, 26-Oct-2006.) (Proof shortened by
Mario Carneiro, 4-Dec-2016.)
|
⊢ (𝑏 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜑} “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 [𝑏 / 𝑦]𝜑) |
|
Theorem | isarep2 5146* |
Part of a study of the Axiom of Replacement used by the Isabelle prover.
In Isabelle, the sethood of PrimReplace is apparently postulated
implicitly by its type signature "[ i,
[ i, i ] => o ]
=> i", which automatically asserts that it is a set without
using any
axioms. To prove that it is a set in Metamath, we need the hypotheses
of Isabelle's "Axiom of Replacement" as well as the Axiom of
Replacement
in the form funimaex 5144. (Contributed by NM, 26-Oct-2006.)
|
⊢ 𝐴 ∈ V & ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧((𝜑 ∧ [𝑧 / 𝑦]𝜑) → 𝑦 = 𝑧) ⇒ ⊢ ∃𝑤 𝑤 = ({〈𝑥, 𝑦〉 ∣ 𝜑} “ 𝐴) |
|
Theorem | fneq1 5147 |
Equality theorem for function predicate with domain. (Contributed by NM,
1-Aug-1994.)
|
⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) |
|
Theorem | fneq2 5148 |
Equality theorem for function predicate with domain. (Contributed by NM,
1-Aug-1994.)
|
⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) |
|
Theorem | fneq1d 5149 |
Equality deduction for function predicate with domain. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) |
|
Theorem | fneq2d 5150 |
Equality deduction for function predicate with domain. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) |
|
Theorem | fneq12d 5151 |
Equality deduction for function predicate with domain. (Contributed by
NM, 26-Jun-2011.)
|
⊢ (𝜑 → 𝐹 = 𝐺)
& ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐵)) |
|
Theorem | fneq12 5152 |
Equality theorem for function predicate with domain. (Contributed by
Thierry Arnoux, 31-Jan-2017.)
|
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐵) → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐵)) |
|
Theorem | fneq1i 5153 |
Equality inference for function predicate with domain. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
⊢ 𝐹 = 𝐺 ⇒ ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴) |
|
Theorem | fneq2i 5154 |
Equality inference for function predicate with domain. (Contributed by
NM, 4-Sep-2011.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵) |
|
Theorem | nffn 5155 |
Bound-variable hypothesis builder for a function with domain.
(Contributed by NM, 30-Jan-2004.)
|
⊢ Ⅎ𝑥𝐹
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝐹 Fn 𝐴 |
|
Theorem | fnfun 5156 |
A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
|
⊢ (𝐹 Fn 𝐴 → Fun 𝐹) |
|
Theorem | fnrel 5157 |
A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)
|
⊢ (𝐹 Fn 𝐴 → Rel 𝐹) |
|
Theorem | fndm 5158 |
The domain of a function. (Contributed by NM, 2-Aug-1994.)
|
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
|
Theorem | funfni 5159 |
Inference to convert a function and domain antecedent. (Contributed by
NM, 22-Apr-2004.)
|
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑) |
|
Theorem | fndmu 5160 |
A function has a unique domain. (Contributed by NM, 11-Aug-1994.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐹 Fn 𝐵) → 𝐴 = 𝐵) |
|
Theorem | fnbr 5161 |
The first argument of binary relation on a function belongs to the
function's domain. (Contributed by NM, 7-May-2004.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵𝐹𝐶) → 𝐵 ∈ 𝐴) |
|
Theorem | fnop 5162 |
The first argument of an ordered pair in a function belongs to the
function's domain. (Contributed by NM, 8-Aug-1994.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 〈𝐵, 𝐶〉 ∈ 𝐹) → 𝐵 ∈ 𝐴) |
|
Theorem | fneu 5163* |
There is exactly one value of a function. (Contributed by NM,
22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ∃!𝑦 𝐵𝐹𝑦) |
|
Theorem | fneu2 5164* |
There is exactly one value of a function. (Contributed by NM,
7-Nov-1995.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ∃!𝑦〈𝐵, 𝑦〉 ∈ 𝐹) |
|
Theorem | fnun 5165 |
The union of two functions with disjoint domains. (Contributed by NM,
22-Sep-2004.)
|
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵)) |
|
Theorem | fnunsn 5166 |
Extension of a function with a new ordered pair. (Contributed by NM,
28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝜑 → 𝑌 ∈ V) & ⊢ (𝜑 → 𝐹 Fn 𝐷)
& ⊢ 𝐺 = (𝐹 ∪ {〈𝑋, 𝑌〉}) & ⊢ 𝐸 = (𝐷 ∪ {𝑋}) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → 𝐺 Fn 𝐸) |
|
Theorem | fnco 5167 |
Composition of two functions. (Contributed by NM, 22-May-2006.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵) |
|
Theorem | fnresdm 5168 |
A function does not change when restricted to its domain. (Contributed by
NM, 5-Sep-2004.)
|
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
|
Theorem | fnresdisj 5169 |
A function restricted to a class disjoint with its domain is empty.
(Contributed by NM, 23-Sep-2004.)
|
⊢ (𝐹 Fn 𝐴 → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐹 ↾ 𝐵) = ∅)) |
|
Theorem | 2elresin 5170 |
Membership in two functions restricted by each other's domain.
(Contributed by NM, 8-Aug-1994.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) ↔ (〈𝑥, 𝑦〉 ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ∧ 〈𝑥, 𝑧〉 ∈ (𝐺 ↾ (𝐴 ∩ 𝐵))))) |
|
Theorem | fnssresb 5171 |
Restriction of a function with a subclass of its domain. (Contributed by
NM, 10-Oct-2007.)
|
⊢ (𝐹 Fn 𝐴 → ((𝐹 ↾ 𝐵) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴)) |
|
Theorem | fnssres 5172 |
Restriction of a function with a subclass of its domain. (Contributed by
NM, 2-Aug-1994.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵) |
|
Theorem | fnresin1 5173 |
Restriction of a function's domain with an intersection. (Contributed by
NM, 9-Aug-1994.)
|
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ (𝐴 ∩ 𝐵)) Fn (𝐴 ∩ 𝐵)) |
|
Theorem | fnresin2 5174 |
Restriction of a function's domain with an intersection. (Contributed by
NM, 9-Aug-1994.)
|
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ (𝐵 ∩ 𝐴)) Fn (𝐵 ∩ 𝐴)) |
|
Theorem | fnres 5175* |
An equivalence for functionality of a restriction. Compare dffun8 5087.
(Contributed by Mario Carneiro, 20-May-2015.)
|
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) |
|
Theorem | fnresi 5176 |
Functionality and domain of restricted identity. (Contributed by NM,
27-Aug-2004.)
|
⊢ ( I ↾ 𝐴) Fn 𝐴 |
|
Theorem | fnima 5177 |
The image of a function's domain is its range. (Contributed by NM,
4-Nov-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
⊢ (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) = ran 𝐹) |
|
Theorem | fn0 5178 |
A function with empty domain is empty. (Contributed by NM, 15-Apr-1998.)
(Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅) |
|
Theorem | fnimadisj 5179 |
A class that is disjoint with the domain of a function has an empty image
under the function. (Contributed by FL, 24-Jan-2007.)
|
⊢ ((𝐹 Fn 𝐴 ∧ (𝐴 ∩ 𝐶) = ∅) → (𝐹 “ 𝐶) = ∅) |
|
Theorem | fnimaeq0 5180 |
Images under a function never map nonempty sets to empty sets.
(Contributed by Stefan O'Rear, 21-Jan-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → ((𝐹 “ 𝐵) = ∅ ↔ 𝐵 = ∅)) |
|
Theorem | dfmpt3 5181 |
Alternate definition for the maps-to notation df-mpt 3931. (Contributed
by Mario Carneiro, 30-Dec-2016.)
|
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪
𝑥 ∈ 𝐴 ({𝑥} × {𝐵}) |
|
Theorem | fnopabg 5182* |
Functionality and domain of an ordered-pair class abstraction.
(Contributed by NM, 30-Jan-2004.) (Proof shortened by Mario Carneiro,
4-Dec-2016.)
|
⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 ↔ 𝐹 Fn 𝐴) |
|
Theorem | fnopab 5183* |
Functionality and domain of an ordered-pair class abstraction.
(Contributed by NM, 5-Mar-1996.)
|
⊢ (𝑥 ∈ 𝐴 → ∃!𝑦𝜑)
& ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⇒ ⊢ 𝐹 Fn 𝐴 |
|
Theorem | mptfng 5184* |
The maps-to notation defines a function with domain. (Contributed by
Scott Fenton, 21-Mar-2011.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴) |
|
Theorem | fnmpt 5185* |
The maps-to notation defines a function with domain. (Contributed by
NM, 9-Apr-2013.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴) |
|
Theorem | mpt0 5186 |
A mapping operation with empty domain. (Contributed by Mario Carneiro,
28-Dec-2014.)
|
⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅ |
|
Theorem | fnmpti 5187* |
Functionality and domain of an ordered-pair class abstraction.
(Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
⊢ 𝐵 ∈ V & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ 𝐹 Fn 𝐴 |
|
Theorem | dmmpti 5188* |
Domain of an ordered-pair class abstraction that specifies a function.
(Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
⊢ 𝐵 ∈ V & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 = 𝐴 |
|
Theorem | dmmptd 5189* |
The domain of the mapping operation, deduction form. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 = 𝐵) |
|
Theorem | mptun 5190 |
Union of mappings which are mutually compatible. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↦ 𝐶) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ∪ (𝑥 ∈ 𝐵 ↦ 𝐶)) |
|
Theorem | feq1 5191 |
Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
|
⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) |
|
Theorem | feq2 5192 |
Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
|
⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) |
|
Theorem | feq3 5193 |
Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
|
⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵)) |
|
Theorem | feq23 5194 |
Equality theorem for functions. (Contributed by FL, 14-Jul-2007.) (Proof
shortened by Andrew Salmon, 17-Sep-2011.)
|
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷)) |
|
Theorem | feq1d 5195 |
Equality deduction for functions. (Contributed by NM, 19-Feb-2008.)
|
⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) |
|
Theorem | feq2d 5196 |
Equality deduction for functions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) |
|
Theorem | feq3d 5197 |
Equality deduction for functions. (Contributed by AV, 1-Jan-2020.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵)) |
|
Theorem | feq12d 5198 |
Equality deduction for functions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
⊢ (𝜑 → 𝐹 = 𝐺)
& ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)) |
|
Theorem | feq123d 5199 |
Equality deduction for functions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
⊢ (𝜑 → 𝐹 = 𝐺)
& ⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐷)) |
|
Theorem | feq123 5200 |
Equality theorem for functions. (Contributed by FL, 16-Nov-2008.)
|
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐶⟶𝐷)) |