Theorem List for Intuitionistic Logic Explorer - 5501-5600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fvco4 5501 |
Value of a composition. (Contributed by BJ, 7-Jul-2022.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif)
![K K](_ck.gif)
![F F](_cf.gif) ![( (](lp.gif)
![( (](lp.gif) ![K K](_ck.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fvopab3g 5502* |
Value of a function given by ordered-pair class abstraction.
(Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](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) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fvopab3ig 5503* |
Value of a function given by ordered-pair class abstraction.
(Contributed by NM, 23-Oct-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif)
![E* E*](_em1.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) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fvmptss2 5504* |
A mapping always evaluates to a subset of the substituted expression in
the mapping, even if this is a proper class, or we are out of the
domain. (Contributed by Mario Carneiro, 13-Feb-2015.) (Revised by
Mario Carneiro, 3-Jul-2019.)
|
![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![D D](_cd.gif)
![C C](_cc.gif) |
|
Theorem | fvmptg 5505* |
Value of a function given in maps-to notation. (Contributed by NM,
2-Oct-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fvmpt 5506* |
Value of a function given in maps-to notation. (Contributed by NM,
17-Aug-2011.)
|
![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fvmpts 5507* |
Value of a function given in maps-to notation, using explicit class
substitution. (Contributed by Scott Fenton, 17-Jul-2013.) (Revised by
Mario Carneiro, 31-Aug-2015.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![V V](_cv.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | fvmpt3 5508* |
Value of a function given in maps-to notation, with a slightly
different sethood condition. (Contributed by Stefan O'Rear,
30-Jan-2015.)
|
![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fvmpt3i 5509* |
Value of a function given in maps-to notation, with a slightly different
sethood condition. (Contributed by Mario Carneiro, 11-Sep-2015.)
|
![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fvmptd 5510* |
Deduction version of fvmpt 5506. (Contributed by Scott Fenton,
18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | mptrcl 5511* |
Reverse closure for a mapping: If the function value of a mapping has a
member, the argument belongs to the base class of the mapping.
(Contributed by AV, 4-Apr-2020.) (Revised by Jim Kingdon,
27-Mar-2023.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![X X](_cx.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fvmpt2 5512* |
Value of a function given by the maps-to notation. (Contributed by FL,
21-Jun-2010.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | fvmptssdm 5513* |
If all the values of the mapping are subsets of a class , then so
is any evaluation of the mapping at a value in the domain of the
mapping. (Contributed by Jim Kingdon, 3-Jan-2018.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif)
![A. A.](forall.gif) ![C C](_cc.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![D D](_cd.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | mptfvex 5514* |
Sufficient condition for a maps-to notation to be set-like.
(Contributed by Mario Carneiro, 3-Jul-2019.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![W W](_cw.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![C C](_cc.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | fvmpt2d 5515* |
Deduction version of fvmpt2 5512. (Contributed by Thierry Arnoux,
8-Dec-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | fvmptdf 5516* |
Alternate deduction version of fvmpt 5506, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fvmptdv 5517* |
Alternate deduction version of fvmpt 5506, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fvmptdv2 5518* |
Alternate deduction version of fvmpt 5506, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mpteqb 5519* |
Bidirectional equality theorem for a mapping abstraction. Equivalent to
eqfnfv 5526. (Contributed by Mario Carneiro,
14-Nov-2014.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif)
![A. A.](forall.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | fvmptt 5520* |
Closed theorem form of fvmpt 5506. (Contributed by Scott Fenton,
21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![V V](_cv.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fvmptf 5521* |
Value of a function given by an ordered-pair class abstraction. This
version of fvmptg 5505 uses bound-variable hypotheses instead of
distinct
variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by
Mario Carneiro, 15-Oct-2016.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fvmptd3 5522* |
Deduction version of fvmpt 5506. (Contributed by Glauco Siliprandi,
23-Oct-2021.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif)
![D D](_cd.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | elfvmptrab1 5523* |
Implications for the value of a function defined by the maps-to notation
with a class abstraction as a result having an element. Here, the base
set of the class abstraction depends on the argument of the function.
(Contributed by Alexander van der Vekens, 15-Jul-2018.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![[_ [_](_ulbrack.gif) ![m m](_m.gif) ![]_ ]_](_urbrack.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) ![( (](lp.gif)
![[_ [_](_ulbrack.gif) ![m m](_m.gif) ![]_ ]_](_urbrack.gif)
![_V _V](rmcv.gif) ![( (](lp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![X X](_cx.gif) ![( (](lp.gif)
![[_ [_](_ulbrack.gif) ![m m](_m.gif) ![]_ ]_](_urbrack.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elfvmptrab 5524* |
Implications for the value of a function defined by the maps-to notation
with a class abstraction as a result having an element. (Contributed by
Alexander van der Vekens, 15-Jul-2018.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) ![( (](lp.gif)
![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![X X](_cx.gif) ![( (](lp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fvopab6 5525* |
Value of a function given by ordered-pair class abstraction.
(Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro,
11-Sep-2015.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | eqfnfv 5526* |
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
(Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon,
22-Oct-2011.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eqfnfv2 5527* |
Equality of functions is determined by their values. Exercise 4 of
[TakeutiZaring] p. 28.
(Contributed by NM, 3-Aug-1994.) (Revised by
Mario Carneiro, 31-Aug-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eqfnfv3 5528* |
Derive equality of functions from equality of their values.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif)
![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eqfnfvd 5529* |
Deduction for equality of functions. (Contributed by Mario Carneiro,
24-Jul-2014.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![) )](rp.gif) |
|
Theorem | eqfnfv2f 5530* |
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
This version of eqfnfv 5526 uses bound-variable hypotheses instead of
distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eqfunfv 5531* |
Equality of functions is determined by their values. (Contributed by
Scott Fenton, 19-Jun-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![( (](lp.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![F F](_cf.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif)
![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fvreseq 5532* |
Equality of restricted functions is determined by their values.
(Contributed by NM, 3-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fndmdif 5533* |
Two ways to express the locus of differences between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![G G](_cg.gif) ![{ {](lbrace.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | fndmdifcom 5534 |
The difference set between two functions is commutative. (Contributed
by Stefan O'Rear, 17-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![G G](_cg.gif) ![( (](lp.gif)
![F F](_cf.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fndmin 5535* |
Two ways to express the locus of equality between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![G G](_cg.gif) ![{ {](lbrace.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | fneqeql 5536 |
Two functions are equal iff their equalizer is the whole domain.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fneqeql2 5537 |
Two functions are equal iff their equalizer contains the whole domain.
(Contributed by Stefan O'Rear, 9-Mar-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif)
![( (](lp.gif) ![G G](_cg.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fnreseql 5538 |
Two functions are equal on a subset iff their equalizer contains that
subset. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![X X](_cx.gif)
![( (](lp.gif) ![G G](_cg.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | chfnrn 5539* |
The range of a choice function (a function that chooses an element from
each member of its domain) is included in the union of its domain.
(Contributed by NM, 31-Aug-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif)
![x x](_x.gif)
![U. U.](bigcup.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | funfvop 5540 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 14-Oct-1996.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | funfvbrb 5541 |
Two ways to say that
is in the domain of .
(Contributed by
Mario Carneiro, 1-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fvimacnvi 5542 |
A member of a preimage is a function value argument. (Contributed by NM,
4-May-2007.)
|
![( (](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) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | fvimacnv 5543 |
The argument of a function value belongs to the preimage of any class
containing the function value. Raph Levien remarks: "This proof is
unsatisfying, because it seems to me that funimass2 5209 could probably be
strengthened to a biconditional." (Contributed by Raph Levien,
20-Nov-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | funimass3 5544 |
A kind of contraposition law that infers an image subclass from a
subclass of a preimage. Raph Levien remarks: "Likely this could
be
proved directly, and fvimacnv 5543 would be the special case of being
a singleton, but it works this way round too." (Contributed by
Raph
Levien, 20-Nov-2006.)
|
![( (](lp.gif) ![( (](lp.gif)
![F F](_cf.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![A A](_ca.gif)
![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | funimass5 5545* |
A subclass of a preimage in terms of function values. (Contributed by
NM, 15-May-2007.)
|
![( (](lp.gif) ![( (](lp.gif)
![F F](_cf.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![B B](_cb.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | funconstss 5546* |
Two ways of specifying that a function is constant on a subdomain.
(Contributed by NM, 8-Mar-2007.)
|
![( (](lp.gif) ![( (](lp.gif)
![F F](_cf.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif)
![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | elpreima 5547 |
Membership in the preimage of a set under a function. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![C C](_cc.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | fniniseg 5548 |
Membership in the preimage of a singleton, under a function. (Contributed
by Mario Carneiro, 12-May-2014.) (Proof shortened by Mario Carneiro,
28-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![C C](_cc.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fncnvima2 5549* |
Inverse images under functions expressed as abstractions. (Contributed
by Stefan O'Rear, 1-Feb-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![B B](_cb.gif)
![{ {](lbrace.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | fniniseg2 5550* |
Inverse point images under functions expressed as abstractions.
(Contributed by Stefan O'Rear, 1-Feb-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif)
![B B](_cb.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | fnniniseg2 5551* |
Support sets of functions expressed as abstractions. (Contributed by
Stefan O'Rear, 1-Feb-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![(
(](lp.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | rexsupp 5552* |
Existential quantification restricted to a support. (Contributed by
Stefan O'Rear, 23-Mar-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![(
(](lp.gif) ![{ {](lbrace.gif) ![Z Z](_cz.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | unpreima 5553 |
Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![A A](_ca.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | inpreima 5554 |
Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Proof shortened by Mario Carneiro, 14-Jun-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![A A](_ca.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | difpreima 5555 |
Preimage of a difference. (Contributed by Mario Carneiro,
14-Jun-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![A A](_ca.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | respreima 5556 |
The preimage of a restricted function. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) !["
"](backquote.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fimacnv 5557 |
The preimage of the codomain of a mapping is the mapping's domain.
(Contributed by FL, 25-Jan-2007.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![B B](_cb.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fnopfv 5558 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 30-Sep-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![<. <.](langle.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | fvelrn 5559 |
A function's value belongs to its range. (Contributed by NM,
14-Oct-1996.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | fnfvelrn 5560 |
A function's value belongs to its range. (Contributed by NM,
15-Oct-1996.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![B B](_cb.gif)
![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | ffvelrn 5561 |
A function's value belongs to its codomain. (Contributed by NM,
12-Aug-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-->
-->](longrightarrow.gif) ![A A](_ca.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![C C](_cc.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ffvelrni 5562 |
A function's value belongs to its codomain. (Contributed by NM,
6-Apr-2005.)
|
![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![C C](_cc.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ffvelrnda 5563 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![C C](_cc.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ffvelrnd 5564 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![C C](_cc.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | rexrn 5565* |
Restricted existential quantification over the range of a function.
(Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario
Carneiro, 20-Aug-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![y y](_y.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![F F](_cf.gif) ![E. E.](exists.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ralrn 5566* |
Restricted universal quantification over the range of a function.
(Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario
Carneiro, 20-Aug-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![y y](_y.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![F F](_cf.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elrnrexdm 5567* |
For any element in the range of a function there is an element in the
domain of the function for which the function value is the element of
the range. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
|
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elrnrexdmb 5568* |
For any element in the range of a function there is an element in the
domain of the function for which the function value is the element of
the range. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
|
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eldmrexrn 5569* |
For any element in the domain of a function there is an element in the
range of the function which is the function value for the element of the
domain. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
|
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![Y Y](_cy.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ralrnmpt 5570* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![F F](_cf.gif) ![A. A.](forall.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | rexrnmpt 5571* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![F F](_cf.gif) ![E. E.](exists.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | dff2 5572 |
Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | dff3im 5573* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![A. A.](forall.gif) ![E! E!](_e1.gif)
![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | dff4im 5574* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![A. A.](forall.gif) ![E! E!](_e1.gif)
![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | dffo3 5575* |
An onto mapping expressed in terms of function values. (Contributed by
NM, 29-Oct-2006.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-onto-> -onto->](onto.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | dffo4 5576* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-onto-> -onto->](onto.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | dffo5 5577* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-onto-> -onto->](onto.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fmpt 5578* |
Functionality of the mapping operation. (Contributed by Mario Carneiro,
26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | f1ompt 5579* |
Express bijection for a mapping operation. (Contributed by Mario
Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![E! E!](_e1.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | fmpti 5580* |
Functionality of the mapping operation. (Contributed by NM,
19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif)
![B B](_cb.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) |
|
Theorem | fvmptelrn 5581* |
The value of a function at a point of its domain belongs to its
codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fmptd 5582* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Mario Carneiro, 13-Jan-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fmpttd 5583* |
Version of fmptd 5582 with inlined definition. Domain and codomain
of the
mapping operation; deduction form. (Contributed by Glauco Siliprandi,
23-Oct-2021.) (Proof shortened by BJ, 16-Aug-2022.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fmpt3d 5584* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Thierry Arnoux, 4-Jun-2017.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.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 | fmptdf 5585* |
A version of fmptd 5582 using bound-variable hypothesis instead of a
distinct variable condition for . (Contributed by Glauco
Siliprandi, 29-Jun-2017.)
|
![F/
F/](finv.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif)
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ffnfv 5586* |
A function maps to a class to which all values belong. (Contributed by
NM, 3-Dec-2003.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ffnfvf 5587 |
A function maps to a class to which all values belong. This version of
ffnfv 5586 uses bound-variable hypotheses instead of
distinct variable
conditions. (Contributed by NM, 28-Sep-2006.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fnfvrnss 5588* |
An upper bound for range determined by function values. (Contributed by
NM, 8-Oct-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif)
![B B](_cb.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | rnmptss 5589* |
The range of an operation given by the maps-to notation as a subset.
(Contributed by Thierry Arnoux, 24-Sep-2017.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fmpt2d 5590* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by NM, 27-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![y y](_y.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 | ffvresb 5591* |
A necessary and sufficient condition for a restricted function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | resflem 5592* |
A lemma to bound the range of a restriction. The conclusion would also
hold with ![( (](lp.gif) ![Y Y](_cy.gif) in place of (provided
does not
occur in ). If
that stronger result is needed, it is however
simpler to use the instance of resflem 5592 where ![( (](lp.gif)
![Y Y](_cy.gif) is
substituted for (in both the conclusion and the third hypothesis).
(Contributed by BJ, 4-Jul-2022.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![V V](_cv.gif) ![--> -->](longrightarrow.gif) ![X X](_cx.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![Y Y](_cy.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![Y Y](_cy.gif) ![) )](rp.gif) |
|
Theorem | f1oresrab 5593* |
Build a bijection between restricted abstract builders, given a
bijection between the base classes, deduction version. (Contributed by
Thierry Arnoux, 17-Aug-2018.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif)
![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![{ {](lbrace.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![: :](colon.gif) ![{ {](lbrace.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![{ {](lbrace.gif) ![ch ch](_chi.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | fmptco 5594* |
Composition of two functions expressed as ordered-pair class
abstractions. If has the equation ( x + 2 ) and the
equation ( 3 * z ) then ![( (](lp.gif) ![F F](_cf.gif) has the equation ( 3 * ( x +
2 ) ) . (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro,
24-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![T T](_ct.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fmptcof 5595* |
Version of fmptco 5594 where needn't be distinct from .
(Contributed by NM, 27-Dec-2014.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif)
![T T](_ct.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![T T](_ct.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fmptcos 5596* |
Composition of two functions expressed as mapping abstractions.
(Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![[_ [_](_ulbrack.gif) ![y y](_y.gif) ![]_ ]_](_urbrack.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cofmpt 5597* |
Express composition of a maps-to function with another function in a
maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![--> -->](longrightarrow.gif) ![D D](_cd.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fcompt 5598* |
Express composition of two functions as a maps-to applying both in
sequence. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened
by Mario Carneiro, 27-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![: :](colon.gif) ![D D](_cd.gif) ![-->
-->](longrightarrow.gif) ![B B](_cb.gif) ![: :](colon.gif) ![C C](_cc.gif) ![-->
-->](longrightarrow.gif) ![D D](_cd.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![` `](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fcoconst 5599 |
Composition with a constant function. (Contributed by Stefan O'Rear,
11-Mar-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif)
![{ {](lbrace.gif) ![Y Y](_cy.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![Y Y](_cy.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fsn 5600 |
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by NM, 10-Dec-2003.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif) ![--> -->](longrightarrow.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |