Theorem List for Intuitionistic Logic Explorer - 5301-5400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | funfvbrb 5301 |
Two ways to say that
is in the domain of .
(Contributed by
Mario Carneiro, 1-May-2014.)
|
|
|
Theorem | fvimacnvi 5302 |
A member of a preimage is a function value argument. (Contributed by NM,
4-May-2007.)
|
|
|
Theorem | fvimacnv 5303 |
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 4997 could probably be
strengthened to a biconditional." (Contributed by Raph Levien,
20-Nov-2006.)
|
|
|
Theorem | funimass3 5304 |
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 5303 would be the special case of being
a singleton, but it works this way round too." (Contributed by
Raph
Levien, 20-Nov-2006.)
|
|
|
Theorem | funimass5 5305* |
A subclass of a preimage in terms of function values. (Contributed by
NM, 15-May-2007.)
|
|
|
Theorem | funconstss 5306* |
Two ways of specifying that a function is constant on a subdomain.
(Contributed by NM, 8-Mar-2007.)
|
|
|
Theorem | elpreima 5307 |
Membership in the preimage of a set under a function. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | fniniseg 5308 |
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.)
|
|
|
Theorem | fncnvima2 5309* |
Inverse images under functions expressed as abstractions. (Contributed
by Stefan O'Rear, 1-Feb-2015.)
|
|
|
Theorem | fniniseg2 5310* |
Inverse point images under functions expressed as abstractions.
(Contributed by Stefan O'Rear, 1-Feb-2015.)
|
|
|
Theorem | fnniniseg2 5311* |
Support sets of functions expressed as abstractions. (Contributed by
Stefan O'Rear, 1-Feb-2015.)
|
|
|
Theorem | rexsupp 5312* |
Existential quantification restricted to a support. (Contributed by
Stefan O'Rear, 23-Mar-2015.)
|
|
|
Theorem | unpreima 5313 |
Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | inpreima 5314 |
Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Proof shortened by Mario Carneiro, 14-Jun-2016.)
|
|
|
Theorem | difpreima 5315 |
Preimage of a difference. (Contributed by Mario Carneiro,
14-Jun-2016.)
|
|
|
Theorem | respreima 5316 |
The preimage of a restricted function. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
|
|
Theorem | fimacnv 5317 |
The preimage of the codomain of a mapping is the mapping's domain.
(Contributed by FL, 25-Jan-2007.)
|
|
|
Theorem | fnopfv 5318 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 30-Sep-2004.)
|
|
|
Theorem | fvelrn 5319 |
A function's value belongs to its range. (Contributed by NM,
14-Oct-1996.)
|
|
|
Theorem | fnfvelrn 5320 |
A function's value belongs to its range. (Contributed by NM,
15-Oct-1996.)
|
|
|
Theorem | ffvelrn 5321 |
A function's value belongs to its codomain. (Contributed by NM,
12-Aug-1999.)
|
|
|
Theorem | ffvelrni 5322 |
A function's value belongs to its codomain. (Contributed by NM,
6-Apr-2005.)
|
|
|
Theorem | ffvelrnda 5323 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
|
|
Theorem | ffvelrnd 5324 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
|
|
Theorem | rexrn 5325* |
Restricted existential quantification over the range of a function.
(Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario
Carneiro, 20-Aug-2014.)
|
|
|
Theorem | ralrn 5326* |
Restricted universal quantification over the range of a function.
(Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario
Carneiro, 20-Aug-2014.)
|
|
|
Theorem | elrnrexdm 5327* |
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.)
|
|
|
Theorem | elrnrexdmb 5328* |
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.)
|
|
|
Theorem | eldmrexrn 5329* |
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.)
|
|
|
Theorem | ralrnmpt 5330* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | rexrnmpt 5331* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | dff2 5332 |
Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
|
|
|
Theorem | dff3im 5333* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
|
|
Theorem | dff4im 5334* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
|
|
Theorem | dffo3 5335* |
An onto mapping expressed in terms of function values. (Contributed by
NM, 29-Oct-2006.)
|
|
|
Theorem | dffo4 5336* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
|
|
Theorem | dffo5 5337* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
|
|
Theorem | foelrn 5338* |
Property of a surjective function. (Contributed by Jeff Madsen,
4-Jan-2011.)
|
|
|
Theorem | foco2 5339 |
If a composition of two functions is surjective, then the function on
the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011.)
|
|
|
Theorem | fmpt 5340* |
Functionality of the mapping operation. (Contributed by Mario Carneiro,
26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | f1ompt 5341* |
Express bijection for a mapping operation. (Contributed by Mario
Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
|
|
Theorem | fmpti 5342* |
Functionality of the mapping operation. (Contributed by NM,
19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
|
|
Theorem | fmptd 5343* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Mario Carneiro, 13-Jan-2013.)
|
|
|
Theorem | ffnfv 5344* |
A function maps to a class to which all values belong. (Contributed by
NM, 3-Dec-2003.)
|
|
|
Theorem | ffnfvf 5345 |
A function maps to a class to which all values belong. This version of
ffnfv 5344 uses bound-variable hypotheses instead of
distinct variable
conditions. (Contributed by NM, 28-Sep-2006.)
|
|
|
Theorem | fnfvrnss 5346* |
An upper bound for range determined by function values. (Contributed by
NM, 8-Oct-2004.)
|
|
|
Theorem | rnmptss 5347* |
The range of an operation given by the "maps to" notation as a
subset.
(Contributed by Thierry Arnoux, 24-Sep-2017.)
|
|
|
Theorem | fmpt2d 5348* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by NM, 27-Dec-2014.)
|
|
|
Theorem | ffvresb 5349* |
A necessary and sufficient condition for a restricted function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
|
|
Theorem | f1oresrab 5350* |
Build a bijection between restricted abstract builders, given a
bijection between the base classes, deduction version. (Contributed by
Thierry Arnoux, 17-Aug-2018.)
|
|
|
Theorem | fmptco 5351* |
Composition of two functions expressed as ordered-pair class
abstractions. If has the equation ( x + 2 ) and the
equation ( 3 * z ) then has the equation ( 3 * ( x +
2 ) ) . (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro,
24-Jul-2014.)
|
|
|
Theorem | fmptcof 5352* |
Version of fmptco 5351 where needn't be distinct from .
(Contributed by NM, 27-Dec-2014.)
|
|
|
Theorem | fmptcos 5353* |
Composition of two functions expressed as mapping abstractions.
(Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
|
|
Theorem | fcompt 5354* |
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.)
|
|
|
Theorem | fcoconst 5355 |
Composition with a constant function. (Contributed by Stefan O'Rear,
11-Mar-2015.)
|
|
|
Theorem | fsn 5356 |
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by NM, 10-Dec-2003.)
|
|
|
Theorem | fsng 5357 |
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by NM, 26-Oct-2012.)
|
|
|
Theorem | fsn2 5358 |
A function that maps a singleton to a class is the singleton of an
ordered pair. (Contributed by NM, 19-May-2004.)
|
|
|
Theorem | xpsng 5359 |
The cross product of two singletons. (Contributed by Mario Carneiro,
30-Apr-2015.)
|
|
|
Theorem | xpsn 5360 |
The cross product of two singletons. (Contributed by NM,
4-Nov-2006.)
|
|
|
Theorem | dfmpt 5361 |
Alternate definition for the "maps to" notation df-mpt 3841 (although it
requires that
be a set). (Contributed by NM, 24-Aug-2010.)
(Revised by Mario Carneiro, 30-Dec-2016.)
|
|
|
Theorem | fnasrn 5362 |
A function expressed as the range of another function. (Contributed by
Mario Carneiro, 22-Jun-2013.) (Proof shortened by Mario Carneiro,
31-Aug-2015.)
|
|
|
Theorem | dfmptg 5363 |
Alternate definition for the "maps to" notation df-mpt 3841 (which requires
that be a set).
(Contributed by Jim Kingdon, 9-Jan-2019.)
|
|
|
Theorem | fnasrng 5364 |
A function expressed as the range of another function. (Contributed by
Jim Kingdon, 9-Jan-2019.)
|
|
|
Theorem | ressnop0 5365 |
If is not in , then the restriction of a
singleton of
to is
null. (Contributed by Scott Fenton,
15-Apr-2011.)
|
|
|
Theorem | fpr 5366 |
A function with a domain of two elements. (Contributed by Jeff Madsen,
20-Jun-2010.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
|
|
Theorem | fprg 5367 |
A function with a domain of two elements. (Contributed by FL,
2-Feb-2014.)
|
|
|
Theorem | ftpg 5368 |
A function with a domain of three elements. (Contributed by Alexander van
der Vekens, 4-Dec-2017.)
|
|
|
Theorem | ftp 5369 |
A function with a domain of three elements. (Contributed by Stefan
O'Rear, 17-Oct-2014.) (Proof shortened by Alexander van der Vekens,
23-Jan-2018.)
|
|
|
Theorem | fnressn 5370 |
A function restricted to a singleton. (Contributed by NM,
9-Oct-2004.)
|
|
|
Theorem | fressnfv 5371 |
The value of a function restricted to a singleton. (Contributed by NM,
9-Oct-2004.)
|
|
|
Theorem | fvconst 5372 |
The value of a constant function. (Contributed by NM, 30-May-1999.)
|
|
|
Theorem | fmptsn 5373* |
Express a singleton function in maps-to notation. (Contributed by NM,
6-Jun-2006.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised
by Stefan O'Rear, 28-Feb-2015.)
|
|
|
Theorem | fmptap 5374* |
Append an additional value to a function. (Contributed by NM,
6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | fmptapd 5375* |
Append an additional value to a function. (Contributed by Thierry
Arnoux, 3-Jan-2017.)
|
|
|
Theorem | fmptpr 5376* |
Express a pair function in maps-to notation. (Contributed by Thierry
Arnoux, 3-Jan-2017.)
|
|
|
Theorem | fvresi 5377 |
The value of a restricted identity function. (Contributed by NM,
19-May-2004.)
|
|
|
Theorem | fvunsng 5378 |
Remove an ordered pair not participating in a function value.
(Contributed by Jim Kingdon, 7-Jan-2019.)
|
|
|
Theorem | fvsn 5379 |
The value of a singleton of an ordered pair is the second member.
(Contributed by NM, 12-Aug-1994.)
|
|
|
Theorem | fvsng 5380 |
The value of a singleton of an ordered pair is the second member.
(Contributed by NM, 26-Oct-2012.)
|
|
|
Theorem | fvsnun1 5381 |
The value of a function with one of its ordered pairs replaced, at the
replaced ordered pair. See also fvsnun2 5382. (Contributed by NM,
23-Sep-2007.)
|
|
|
Theorem | fvsnun2 5382 |
The value of a function with one of its ordered pairs replaced, at
arguments other than the replaced one. See also fvsnun1 5381.
(Contributed by NM, 23-Sep-2007.)
|
|
|
Theorem | fsnunf 5383 |
Adjoining a point to a function gives a function. (Contributed by Stefan
O'Rear, 28-Feb-2015.)
|
|
|
Theorem | fsnunfv 5384 |
Recover the added point from a point-added function. (Contributed by
Stefan O'Rear, 28-Feb-2015.) (Revised by NM, 18-May-2017.)
|
|
|
Theorem | fsnunres 5385 |
Recover the original function from a point-added function. (Contributed
by Stefan O'Rear, 28-Feb-2015.)
|
|
|
Theorem | fvpr1 5386 |
The value of a function with a domain of two elements. (Contributed by
Jeff Madsen, 20-Jun-2010.)
|
|
|
Theorem | fvpr2 5387 |
The value of a function with a domain of two elements. (Contributed by
Jeff Madsen, 20-Jun-2010.)
|
|
|
Theorem | fvpr1g 5388 |
The value of a function with a domain of (at most) two elements.
(Contributed by Alexander van der Vekens, 3-Dec-2017.)
|
|
|
Theorem | fvpr2g 5389 |
The value of a function with a domain of (at most) two elements.
(Contributed by Alexander van der Vekens, 3-Dec-2017.)
|
|
|
Theorem | fvtp1g 5390 |
The value of a function with a domain of (at most) three elements.
(Contributed by Alexander van der Vekens, 4-Dec-2017.)
|
|
|
Theorem | fvtp2g 5391 |
The value of a function with a domain of (at most) three elements.
(Contributed by Alexander van der Vekens, 4-Dec-2017.)
|
|
|
Theorem | fvtp3g 5392 |
The value of a function with a domain of (at most) three elements.
(Contributed by Alexander van der Vekens, 4-Dec-2017.)
|
|
|
Theorem | fvtp1 5393 |
The first value of a function with a domain of three elements.
(Contributed by NM, 14-Sep-2011.)
|
|
|
Theorem | fvtp2 5394 |
The second value of a function with a domain of three elements.
(Contributed by NM, 14-Sep-2011.)
|
|
|
Theorem | fvtp3 5395 |
The third value of a function with a domain of three elements.
(Contributed by NM, 14-Sep-2011.)
|
|
|
Theorem | fvconst2g 5396 |
The value of a constant function. (Contributed by NM, 20-Aug-2005.)
|
|
|
Theorem | fconst2g 5397 |
A constant function expressed as a cross product. (Contributed by NM,
27-Nov-2007.)
|
|
|
Theorem | fvconst2 5398 |
The value of a constant function. (Contributed by NM, 16-Apr-2005.)
|
|
|
Theorem | fconst2 5399 |
A constant function expressed as a cross product. (Contributed by NM,
20-Aug-1999.)
|
|
|
Theorem | fconstfvm 5400* |
A constant function expressed in terms of its functionality, domain, and
value. See also fconst2 5399. (Contributed by Jim Kingdon,
8-Jan-2019.)
|
|