![]() |
Intuitionistic Logic Explorer Theorem List (p. 53 of 149) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iotacl 5201 |
Membership law for descriptions.
This can useful for expanding an unbounded iota-based definition (see df-iota 5178). (Contributed by Andrew Salmon, 1-Aug-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | iota2df 5202 |
A condition that allows us to represent "the unique element such that
![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | iota2d 5203* |
A condition that allows us to represent "the unique element such that
![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eliota 5204* | An element of an iota expression. (Contributed by Jim Kingdon, 22-Nov-2024.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eliotaeu 5205 | An inhabited iota expression has a unique value. (Contributed by Jim Kingdon, 22-Nov-2024.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | iota2 5206* |
The unique element such that ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | sniota 5207 | A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | iotam 5208* |
Representation of "the unique element such that ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | csbiotag 5209* | Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | wfun 5210 |
Extend the definition of a wff to include the function predicate. (Read:
![]() |
![]() ![]() ![]() | ||
Syntax | wfn 5211 |
Extend the definition of a wff to include the function predicate with a
domain. (Read: ![]() ![]() |
![]() ![]() ![]() ![]() | ||
Syntax | wf 5212 |
Extend the definition of a wff to include the function predicate with
domain and codomain. (Read: ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | wf1 5213 |
Extend the definition of a wff to include one-to-one functions. (Read:
![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | wfo 5214 |
Extend the definition of a wff to include onto functions. (Read: ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | wf1o 5215 |
Extend the definition of a wff to include one-to-one onto functions.
(Read: ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | cfv 5216 |
Extend the definition of a class to include the value of a function.
(Read: The value of ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | wiso 5217 |
Extend the definition of a wff to include the isomorphism property.
(Read: ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-fun 5218 |
Define predicate that determines if some class ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-fn 5219 | Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-f 5220 | Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-f1 5221 | Define a one-to-one function. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by NM, 1-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-fo 5222 | Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). (Contributed by NM, 1-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-f1o 5223 | Define a one-to-one onto function. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by NM, 1-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-fv 5224* |
Define the value of a function, ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-isom 5225* |
Define the isomorphism predicate. We read this as "![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | dffun2 5226* | Alternate definition of a function. (Contributed by NM, 29-Dec-1996.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | dffun4 5227* | Alternate definition of a function. Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 29-Dec-1996.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | dffun5r 5228* | A way of proving a relation is a function, analogous to mo2r 2078. (Contributed by Jim Kingdon, 27-May-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | dffun6f 5229* | Definition of function, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 15-Oct-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | dffun6 5230* | Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funmo 5231* | A function has at most one value for each argument. (Contributed by NM, 24-May-1998.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | dffun4f 5232* | Definition of function like dffun4 5227 but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Jim Kingdon, 17-Mar-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funrel 5233 | A function is a relation. (Contributed by NM, 1-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 0nelfun 5234 | A function does not contain the empty set. (Contributed by BJ, 26-Nov-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funss 5235 | Subclass theorem for function predicate. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funeq 5236 | Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funeqi 5237 | Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funeqd 5238 | Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nffun 5239 | Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | sbcfung 5240 | Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funeu 5241* | There is exactly one value of a function. (Contributed by NM, 22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funeu2 5242* | There is exactly one value of a function. (Contributed by NM, 3-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | dffun7 5243* | Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. (Enderton's definition is ambiguous because "there is only one" could mean either "there is at most one" or "there is exactly one". However, dffun8 5244 shows that it does not matter which meaning we pick.) (Contributed by NM, 4-Nov-2002.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | dffun8 5244* | Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 5243. (Contributed by NM, 4-Nov-2002.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | dffun9 5245* | Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funfn 5246 | An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funfnd 5247 | A function is a function over its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funi 5248 | The identity relation is a function. Part of Theorem 10.4 of [Quine] p. 65. (Contributed by NM, 30-Apr-1998.) |
![]() ![]() ![]() | ||
Theorem | nfunv 5249 | The universe is not a function. (Contributed by Raph Levien, 27-Jan-2004.) |
![]() ![]() ![]() ![]() | ||
Theorem | funopg 5250 | A Kuratowski ordered pair is a function only if its components are equal. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funopab 5251* | A class of ordered pairs is a function when there is at most one second member for each pair. (Contributed by NM, 16-May-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funopabeq 5252* | A class of ordered pairs of values is a function. (Contributed by NM, 14-Nov-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funopab4 5253* | A class of ordered pairs of values in the form used by df-mpt 4066 is a function. (Contributed by NM, 17-Feb-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funmpt 5254 | A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funmpt2 5255 | Functionality of a class given by a maps-to notation. (Contributed by FL, 17-Feb-2008.) (Revised by Mario Carneiro, 31-May-2014.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funco 5256 | The composition of two functions is a function. Exercise 29 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funres 5257 | A restriction of a function is a function. Compare Exercise 18 of [TakeutiZaring] p. 25. (Contributed by NM, 16-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funssres 5258 | The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fun2ssres 5259 | Equality of restrictions of a function and a subclass. (Contributed by NM, 16-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funun 5260 | The union of functions with disjoint domains is a function. Theorem 4.6 of [Monk1] p. 43. (Contributed by NM, 12-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funcnvsn 5261 |
The converse singleton of an ordered pair is a function. This is
equivalent to funsn 5264 via cnvsn 5111, but stating it this way allows us to
skip the sethood assumptions on ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funsng 5262 | A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 28-Jun-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fnsng 5263 | Functionality and domain of the singleton of an ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funsn 5264 | A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 12-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funinsn 5265 |
A function based on the singleton of an ordered pair. Unlike funsng 5262,
this holds even if ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funprg 5266 | A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funtpg 5267 | A set of three pairs is a function if their first members are different. (Contributed by Alexander van der Vekens, 5-Dec-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funpr 5268 | A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funtp 5269 | A function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fnsn 5270 | Functionality and domain of the singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fnprg 5271 | Function with a domain of two different values. (Contributed by FL, 26-Jun-2011.) (Revised by Mario Carneiro, 26-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fntpg 5272 | Function with a domain of three different values. (Contributed by Alexander van der Vekens, 5-Dec-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fntp 5273 | A function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) (Revised by Mario Carneiro, 26-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fun0 5274 | The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed by NM, 7-Apr-1998.) |
![]() ![]() ![]() | ||
Theorem | funcnvcnv 5275 | The double converse of a function is a function. (Contributed by NM, 21-Sep-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funcnv2 5276* | A simpler equivalence for single-rooted (see funcnv 5277). (Contributed by NM, 9-Aug-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funcnv 5277* |
The converse of a class is a function iff the class is single-rooted,
which means that for any ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funcnv3 5278* | A condition showing a class is single-rooted. (See funcnv 5277). (Contributed by NM, 26-May-2006.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funcnveq 5279* | Another way of expressing that a class is single-rooted. Counterpart to dffun2 5226. (Contributed by Jim Kingdon, 24-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fun2cnv 5280* |
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 ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | svrelfun 5281 | A single-valued relation is a function. (See fun2cnv 5280 for "single-valued.") Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 17-Jan-2006.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fncnv 5282* | Single-rootedness (see funcnv 5277) of a class cut down by a cross product. (Contributed by NM, 5-Mar-2007.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fun11 5283* |
Two ways of stating that ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fununi 5284* | The union of a chain (with respect to inclusion) of functions is a function. (Contributed by NM, 10-Aug-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funcnvuni 5285* | The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 5277 for "single-rooted" definition.) (Contributed by NM, 11-Aug-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fun11uni 5286* | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funin 5287 | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funres11 5288 | The restriction of a one-to-one function is one-to-one. (Contributed by NM, 25-Mar-1998.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funcnvres 5289 | The converse of a restricted function. (Contributed by NM, 27-Mar-1998.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cnvresid 5290 | Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funcnvres2 5291 | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funimacnv 5292 | The image of the preimage of a function. (Contributed by NM, 25-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funimass1 5293 | A kind of contraposition law that infers a subclass of an image from a preimage subclass. (Contributed by NM, 25-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funimass2 5294 | A kind of contraposition law that infers an image subclass from a subclass of a preimage. (Contributed by NM, 25-May-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | imadiflem 5295 |
One direction of imadif 5296. This direction does not require
![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | imadif 5296 | The image of a difference is the difference of images. (Contributed by NM, 24-May-1998.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | imainlem 5297 |
One direction of imain 5298. This direction does not require
![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | imain 5298 | The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funimaexglem 5299 |
Lemma for funimaexg 5300. It constitutes the interesting part of
funimaexg 5300, in which ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | funimaexg 5300 | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |