Theorem List for Intuitionistic Logic Explorer - 5201-5300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fun11uni 5201* |
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.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![U. U.](bigcup.gif) ![`' `'](_cnv.gif) ![U.
U.](bigcup.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | funin 5202 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | funres11 5203 |
The restriction of a one-to-one function is one-to-one. (Contributed by
NM, 25-Mar-1998.)
|
![( (](lp.gif) ![`' `'](_cnv.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | funcnvres 5204 |
The converse of a restricted function. (Contributed by NM,
27-Mar-1998.)
|
![( (](lp.gif) ![`' `'](_cnv.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cnvresid 5205 |
Converse of a restricted identity function. (Contributed by FL,
4-Mar-2007.)
|
![`' `'](_cnv.gif)
![A A](_ca.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | funcnvres2 5206 |
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.)
|
![( (](lp.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | funimacnv 5207 |
The image of the preimage of a function. (Contributed by NM,
25-May-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif)
![F F](_cf.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | funimass1 5208 |
A kind of contraposition law that infers a subclass of an image from a
preimage subclass. (Contributed by NM, 25-May-2004.)
|
![( (](lp.gif) ![( (](lp.gif)
![F F](_cf.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![A A](_ca.gif)
![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | funimass2 5209 |
A kind of contraposition law that infers an image subclass from a subclass
of a preimage. (Contributed by NM, 25-May-2004.)
|
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | imadiflem 5210 |
One direction of imadif 5211. This direction does not require
![`' `'](_cnv.gif) . (Contributed by Jim Kingdon,
25-Dec-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![A A](_ca.gif)
![( (](lp.gif) ![F F](_cf.gif) !["
"](backquote.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | imadif 5211 |
The image of a difference is the difference of images. (Contributed by
NM, 24-May-1998.)
|
![( (](lp.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) !["
"](backquote.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | imainlem 5212 |
One direction of imain 5213. This direction does not require
![`' `'](_cnv.gif) . (Contributed by Jim Kingdon,
25-Dec-2018.)
|
![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) !["
"](backquote.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | imain 5213 |
The image of an intersection is the intersection of images.
(Contributed by Paul Chapman, 11-Apr-2009.)
|
![( (](lp.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) !["
"](backquote.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | funimaexglem 5214 |
Lemma for funimaexg 5215. It constitutes the interesting part of
funimaexg 5215, in which
. (Contributed by Jim
Kingdon,
27-Dec-2018.)
|
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![A A](_ca.gif) ![" "](backquote.gif) ![B B](_cb.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | funimaexg 5215 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![" "](backquote.gif) ![B B](_cb.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | funimaex 5216 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![" "](backquote.gif) ![B B](_cb.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | isarep1 5217* |
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 ![ph ph](_varphi.gif) ![( (](lp.gif) ![x x](_x.gif) ![y y](_y.gif) i.e. the class ![( (](lp.gif) ![{ {](lbrace.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) ![" "](backquote.gif) ![A A](_ca.gif) .
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) ![" "](backquote.gif) ![A A](_ca.gif)
![E. E.](exists.gif) ![[ [](lbrack.gif)
![y y](_y.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | isarep2 5218* |
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 5216. (Contributed by NM, 26-Oct-2006.)
|
![A. A.](forall.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![[
[](lbrack.gif) ![y y](_y.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![z z](_z.gif) ![E.
E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) ![" "](backquote.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fneq1 5219 |
Equality theorem for function predicate with domain. (Contributed by NM,
1-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fneq2 5220 |
Equality theorem for function predicate with domain. (Contributed by NM,
1-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fneq1d 5221 |
Equality deduction for function predicate with domain. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
![( (](lp.gif) ![G G](_cg.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fneq2d 5222 |
Equality deduction for function predicate with domain. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fneq12d 5223 |
Equality deduction for function predicate with domain. (Contributed by
NM, 26-Jun-2011.)
|
![( (](lp.gif) ![G G](_cg.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fneq12 5224 |
Equality theorem for function predicate with domain. (Contributed by
Thierry Arnoux, 31-Jan-2017.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fneq1i 5225 |
Equality inference for function predicate with domain. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fneq2i 5226 |
Equality inference for function predicate with domain. (Contributed by
NM, 4-Sep-2011.)
|
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | nffn 5227 |
Bound-variable hypothesis builder for a function with domain.
(Contributed by NM, 30-Jan-2004.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/ F/](finv.gif) ![A A](_ca.gif) |
|
Theorem | fnfun 5228 |
A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
|
![( (](lp.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | fnrel 5229 |
A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)
|
![( (](lp.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | fndm 5230 |
The domain of a function. (Contributed by NM, 2-Aug-1994.)
|
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | funfni 5231 |
Inference to convert a function and domain antecedent. (Contributed by
NM, 22-Apr-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | fndmu 5232 |
A function has a unique domain. (Contributed by NM, 11-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | fnbr 5233 |
The first argument of binary relation on a function belongs to the
function's domain. (Contributed by NM, 7-May-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fnop 5234 |
The first argument of an ordered pair in a function belongs to the
function's domain. (Contributed by NM, 8-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![F F](_cf.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fneu 5235* |
There is exactly one value of a function. (Contributed by NM,
22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![E! E!](_e1.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) |
|
Theorem | fneu2 5236* |
There is exactly one value of a function. (Contributed by NM,
7-Nov-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![<. <.](langle.gif) ![B B](_cb.gif) ![y y](_y.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | fnun 5237 |
The union of two functions with disjoint domains. (Contributed by NM,
22-Sep-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![(/) (/)](varnothing.gif)
![( (](lp.gif) ![G G](_cg.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fnunsn 5238 |
Extension of a function with a new ordered pair. (Contributed by NM,
28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![X X](_cx.gif) ![Y Y](_cy.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![X X](_cx.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif)
![E E](_ce.gif) ![) )](rp.gif) |
|
Theorem | fnco 5239 |
Composition of two functions. (Contributed by NM, 22-May-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![G G](_cg.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | fnresdm 5240 |
A function does not change when restricted to its domain. (Contributed by
NM, 5-Sep-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | fnresdisj 5241 |
A function restricted to a class disjoint with its domain is empty.
(Contributed by NM, 23-Sep-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 2elresin 5242 |
Membership in two functions restricted by each other's domain.
(Contributed by NM, 8-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![z z](_z.gif) ![G G](_cg.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![<. <.](langle.gif) ![x x](_x.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fnssresb 5243 |
Restriction of a function with a subclass of its domain. (Contributed by
NM, 10-Oct-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fnssres 5244 |
Restriction of a function with a subclass of its domain. (Contributed by
NM, 2-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | fnresin1 5245 |
Restriction of a function's domain with an intersection. (Contributed by
NM, 9-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fnresin2 5246 |
Restriction of a function's domain with an intersection. (Contributed by
NM, 9-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fnres 5247* |
An equivalence for functionality of a restriction. Compare dffun8 5159.
(Contributed by Mario Carneiro, 20-May-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![A. A.](forall.gif) ![E! E!](_e1.gif)
![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) |
|
Theorem | fnresi 5248 |
Functionality and domain of restricted identity. (Contributed by NM,
27-Aug-2004.)
|
![A A](_ca.gif) ![A A](_ca.gif) |
|
Theorem | fnima 5249 |
The image of a function's domain is its range. (Contributed by NM,
4-Nov-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![A A](_ca.gif)
![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | fn0 5250 |
A function with empty domain is empty. (Contributed by NM, 15-Apr-1998.)
(Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
![( (](lp.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | fnimadisj 5251 |
A class that is disjoint with the domain of a function has an empty image
under the function. (Contributed by FL, 24-Jan-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![C C](_cc.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | fnimaeq0 5252 |
Images under a function never map nonempty sets to empty sets.
(Contributed by Stefan O'Rear, 21-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) !["
"](backquote.gif) ![B B](_cb.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | dfmpt3 5253 |
Alternate definition for the maps-to notation df-mpt 3999. (Contributed
by Mario Carneiro, 30-Dec-2016.)
|
![( (](lp.gif) ![B B](_cb.gif)
![U_ U_](_cupbar.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | fnopabg 5254* |
Functionality and domain of an ordered-pair class abstraction.
(Contributed by NM, 30-Jan-2004.) (Proof shortened by Mario Carneiro,
4-Dec-2016.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fnopab 5255* |
Functionality and domain of an ordered-pair class abstraction.
(Contributed by NM, 5-Mar-1996.)
|
![( (](lp.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![A A](_ca.gif) |
|
Theorem | mptfng 5256* |
The maps-to notation defines a function with domain. (Contributed by
Scott Fenton, 21-Mar-2011.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fnmpt 5257* |
The maps-to notation defines a function with domain. (Contributed by
NM, 9-Apr-2013.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | mpt0 5258 |
A mapping operation with empty domain. (Contributed by Mario Carneiro,
28-Dec-2014.)
|
![( (](lp.gif) ![A A](_ca.gif) ![(/) (/)](varnothing.gif) |
|
Theorem | fnmpti 5259* |
Functionality and domain of an ordered-pair class abstraction.
(Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
![( (](lp.gif) ![B B](_cb.gif) ![A A](_ca.gif) |
|
Theorem | dmmpti 5260* |
Domain of an ordered-pair class abstraction that specifies a function.
(Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
![( (](lp.gif) ![B B](_cb.gif)
![A A](_ca.gif) |
|
Theorem | dmmptd 5261* |
The domain of the mapping operation, deduction form. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![V V](_cv.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | mptun 5262 |
Union of mappings which are mutually compatible. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | feq1 5263 |
Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![G G](_cg.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | feq2 5264 |
Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![F F](_cf.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | feq3 5265 |
Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![--> -->](longrightarrow.gif) ![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | feq23 5266 |
Equality theorem for functions. (Contributed by FL, 14-Jul-2007.) (Proof
shortened by Andrew Salmon, 17-Sep-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-->
-->](longrightarrow.gif) ![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![--> -->](longrightarrow.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | feq1d 5267 |
Equality deduction for functions. (Contributed by NM, 19-Feb-2008.)
|
![( (](lp.gif) ![G G](_cg.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![G G](_cg.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | feq2d 5268 |
Equality deduction for functions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![F F](_cf.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | feq3d 5269 |
Equality deduction for functions. (Contributed by AV, 1-Jan-2020.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![X X](_cx.gif) ![--> -->](longrightarrow.gif) ![F F](_cf.gif) ![: :](colon.gif) ![X X](_cx.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | feq12d 5270 |
Equality deduction for functions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
![( (](lp.gif) ![G G](_cg.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![G G](_cg.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | feq123d 5271 |
Equality deduction for functions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
![( (](lp.gif) ![G G](_cg.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![G G](_cg.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | feq123 5272 |
Equality theorem for functions. (Contributed by FL, 16-Nov-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![G G](_cg.gif) ![: :](colon.gif) ![C C](_cc.gif) ![--> -->](longrightarrow.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | feq1i 5273 |
Equality inference for functions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-->
-->](longrightarrow.gif) ![G G](_cg.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | feq2i 5274 |
Equality inference for functions. (Contributed by NM, 5-Sep-2011.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-->
-->](longrightarrow.gif) ![F F](_cf.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | feq23i 5275 |
Equality inference for functions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![--> -->](longrightarrow.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | feq23d 5276 |
Equality deduction for functions. (Contributed by NM, 8-Jun-2013.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![--> -->](longrightarrow.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nff 5277 |
Bound-variable hypothesis builder for a mapping. (Contributed by NM,
29-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/
F/](finv.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-->
-->](longrightarrow.gif) ![B B](_cb.gif) |
|
Theorem | sbcfng 5278* |
Distribute proper substitution through the function predicate with a
domain. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sbcfg 5279* |
Distribute proper substitution through the function predicate with
domain and codomain. (Contributed by Alexander van der Vekens,
15-Jul-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![[_
[_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![F F](_cf.gif) ![: :](colon.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ffn 5280 |
A mapping is a function. (Contributed by NM, 2-Aug-1994.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ffnd 5281 |
A mapping is a function with domain, deduction form. (Contributed by
Glauco Siliprandi, 17-Aug-2020.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | dffn2 5282 |
Any function is a mapping into . (Contributed by NM, 31-Oct-1995.)
(Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | ffun 5283 |
A mapping is a function. (Contributed by NM, 3-Aug-1994.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif)
![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | ffund 5284 |
A mapping is a function, deduction version. (Contributed by Glauco
Siliprandi, 3-Mar-2021.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F
F](_cf.gif) ![) )](rp.gif) |
|
Theorem | frel 5285 |
A mapping is a relation. (Contributed by NM, 3-Aug-1994.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif)
![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | fdm 5286 |
The domain of a mapping. (Contributed by NM, 2-Aug-1994.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fdmd 5287 |
Deduction form of fdm 5286. The domain of a mapping. (Contributed by
Glauco Siliprandi, 26-Jun-2021.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fdmi 5288 |
The domain of a mapping. (Contributed by NM, 28-Jul-2008.)
|
![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif)
![A A](_ca.gif) |
|
Theorem | frn 5289 |
The range of a mapping. (Contributed by NM, 3-Aug-1994.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | frnd 5290 |
Deduction form of frn 5289. The range of a mapping. (Contributed by
Glauco Siliprandi, 26-Jun-2021.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | dffn3 5291 |
A function maps to its range. (Contributed by NM, 1-Sep-1999.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | fss 5292 |
Expanding the codomain of a mapping. (Contributed by NM, 10-May-1998.)
(Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-->
-->](longrightarrow.gif) ![C C](_cc.gif)
![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-->
-->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fssd 5293 |
Expanding the codomain of a mapping, deduction form. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fssdmd 5294 |
Expressing that a class is a subclass of the domain of a function
expressed in maps-to notation, deduction form. (Contributed by AV,
21-Aug-2022.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fssdm 5295 |
Expressing that a class is a subclass of the domain of a function
expressed in maps-to notation, semi-deduction form. (Contributed by AV,
21-Aug-2022.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fco 5296 |
Composition of two mappings. (Contributed by NM, 29-Aug-1999.) (Proof
shortened by Andrew Salmon, 17-Sep-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-->
-->](longrightarrow.gif) ![G G](_cg.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-->
-->](longrightarrow.gif) ![B B](_cb.gif) ![( (](lp.gif) ![G G](_cg.gif) ![) )](rp.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fco2 5297 |
Functionality of a composition with weakened out of domain condition on
the first argument. (Contributed by Stefan O'Rear, 11-Mar-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![G G](_cg.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif)
![( (](lp.gif) ![G G](_cg.gif) ![) )](rp.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fssxp 5298 |
A mapping is a class of ordered pairs. (Contributed by NM, 3-Aug-1994.)
(Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fex2 5299 |
A function with bounded domain and range is a set. This version is proven
without the Axiom of Replacement. (Contributed by Mario Carneiro,
24-Jun-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-->
-->](longrightarrow.gif) ![W W](_cw.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | funssxp 5300 |
Two ways of specifying a partial function from to .
(Contributed by NM, 13-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![F F](_cf.gif) ![--> -->](longrightarrow.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |