Home | Metamath
Proof Explorer Theorem List (p. 55 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | opelres 5401 | Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 13-Nov-1995.) |
Theorem | brres 5402 | Binary relation on a restriction. (Contributed by NM, 12-Dec-2006.) |
Theorem | dfres3 5403 | Alternate definition of restriction. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | opelresg 5404 | Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 14-Oct-2005.) |
Theorem | brresg 5405 | Binary relation on a restriction. (Contributed by Mario Carneiro, 4-Nov-2015.) |
Theorem | opres 5406 | Ordered pair membership in a restriction when the first member belongs to the restricting class. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | resieq 5407 | A restricted identity relation is equivalent to equality in its domain. (Contributed by NM, 30-Apr-2004.) |
Theorem | opelresi 5408 | belongs to a restriction of the identity class iff belongs to the restricting class. (Contributed by FL, 27-Oct-2008.) (Revised by NM, 30-Mar-2016.) |
Theorem | resres 5409 | The restriction of a restriction. (Contributed by NM, 27-Mar-2008.) |
Theorem | resundi 5410 | Distributive law for restriction over union. Theorem 31 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.) |
Theorem | resundir 5411 | Distributive law for restriction over union. (Contributed by NM, 23-Sep-2004.) |
Theorem | resindi 5412 | Class restriction distributes over intersection. (Contributed by FL, 6-Oct-2008.) |
Theorem | resindir 5413 | Class restriction distributes over intersection. (Contributed by NM, 18-Dec-2008.) |
Theorem | inres 5414 | Move intersection into class restriction. (Contributed by NM, 18-Dec-2008.) |
Theorem | resdifcom 5415 | Commutative law for restriction and difference. (Contributed by AV, 7-Jun-2021.) |
Theorem | resiun1 5416* | Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015.) (Proof shortened by JJ, 25-Aug-2021.) |
Theorem | resiun1OLD 5417* | Obsolete proof of resiun1 5416 as of 25-Aug-2021. (Contributed by Mario Carneiro, 29-May-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | resiun2 5418* | Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015.) |
Theorem | dmres 5419 | The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by NM, 1-Aug-1994.) |
Theorem | ssdmres 5420 | A domain restricted to a subclass equals the subclass. (Contributed by NM, 2-Mar-1997.) |
Theorem | dmresexg 5421 | The domain of a restriction to a set exists. (Contributed by NM, 7-Apr-1995.) |
Theorem | resss 5422 | A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) |
Theorem | rescom 5423 | Commutative law for restriction. (Contributed by NM, 27-Mar-1998.) |
Theorem | ssres 5424 | Subclass theorem for restriction. (Contributed by NM, 16-Aug-1994.) |
Theorem | ssres2 5425 | Subclass theorem for restriction. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | relres 5426 | A restriction is a relation. Exercise 12 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | resabs1 5427 | Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25. (Contributed by NM, 9-Aug-1994.) |
Theorem | resabs1d 5428 | Absorption law for restriction, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | resabs2 5429 | Absorption law for restriction. (Contributed by NM, 27-Mar-1998.) |
Theorem | residm 5430 | Idempotent law for restriction. (Contributed by NM, 27-Mar-1998.) |
Theorem | resima 5431 | A restriction to an image. (Contributed by NM, 29-Sep-2004.) |
Theorem | resima2 5432 | Image under a restricted class. (Contributed by FL, 31-Aug-2009.) (Proof shortened by JJ, 25-Aug-2021.) |
Theorem | resima2OLD 5433 | Obsolete proof of resima2 5432 as of 25-Aug-2021. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | xpssres 5434 | Restriction of a constant function (or other Cartesian product). (Contributed by Stefan O'Rear, 24-Jan-2015.) |
Theorem | elres 5435* | Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011.) |
Theorem | elsnres 5436* | Membership in restriction to a singleton. (Contributed by Scott Fenton, 17-Mar-2011.) |
Theorem | relssres 5437 | Simplification law for restriction. (Contributed by NM, 16-Aug-1994.) |
Theorem | dmressnsn 5438 | The domain of a restriction to a singleton is a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
Theorem | eldmressnsn 5439 | The element of the domain of a restriction to a singleton is the element of the singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
Theorem | eldmeldmressn 5440 | An element of the domain (of a relation) is an element of the domain of the restriction (of the relation) to the singleton containing this element. (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
Theorem | resdm 5441 | A relation restricted to its domain equals itself. (Contributed by NM, 12-Dec-2006.) |
Theorem | resexg 5442 | The restriction of a set is a set. (Contributed by NM, 28-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | resex 5443 | The restriction of a set is a set. (Contributed by Jeff Madsen, 19-Jun-2011.) |
Theorem | resindm 5444 | When restricting a relation, intersecting with the domain of the relation has no effect. (Contributed by FL, 6-Oct-2008.) |
Theorem | resdmdfsn 5445 | Restricting a relation to its domain without a set is the same as restricting the relation to the universe without this set. (Contributed by AV, 2-Dec-2018.) |
Theorem | resopab 5446* | Restriction of a class abstraction of ordered pairs. (Contributed by NM, 5-Nov-2002.) |
Theorem | iss 5447 | A subclass of the identity function is the identity function restricted to its domain. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | resopab2 5448* | Restriction of a class abstraction of ordered pairs. (Contributed by NM, 24-Aug-2007.) |
Theorem | resmpt 5449* | Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.) |
Theorem | resmpt3 5450* | Unconditional restriction of the mapping operation. (Contributed by Stefan O'Rear, 24-Jan-2015.) (Proof shortened by Mario Carneiro, 22-Mar-2015.) |
Theorem | resmptf 5451 | Restriction of the mapping operation. (Contributed by Thierry Arnoux, 28-Mar-2017.) |
Theorem | resmptd 5452* | Restriction of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | dfres2 5453* | Alternate definition of the restriction operation. (Contributed by Mario Carneiro, 5-Nov-2013.) |
Theorem | mptss 5454* | Sufficient condition for inclusion in map-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Theorem | opabresid 5455* | The restricted identity expressed with the class builder. (Contributed by FL, 25-Apr-2012.) |
Theorem | mptresid 5456* | The restricted identity expressed with the "maps to" notation. (Contributed by FL, 25-Apr-2012.) |
Theorem | dmresi 5457 | The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004.) |
Theorem | restidsing 5458 | Restriction of the identity to a singleton. (Contributed by FL, 2-Aug-2009.) (Proof shortened by JJ, 25-Aug-2021.) |
Theorem | restidsingOLD 5459 | Obsolete proof of restidsing 5458 as of 25-Aug-2021. (Contributed by FL, 2-Aug-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | resid 5460 | Any relation restricted to the universe is itself. (Contributed by NM, 16-Mar-2004.) |
Theorem | imaeq1 5461 | Equality theorem for image. (Contributed by NM, 14-Aug-1994.) |
Theorem | imaeq2 5462 | Equality theorem for image. (Contributed by NM, 14-Aug-1994.) |
Theorem | imaeq1i 5463 | Equality theorem for image. (Contributed by NM, 21-Dec-2008.) |
Theorem | imaeq2i 5464 | Equality theorem for image. (Contributed by NM, 21-Dec-2008.) |
Theorem | imaeq1d 5465 | Equality theorem for image. (Contributed by FL, 15-Dec-2006.) |
Theorem | imaeq2d 5466 | Equality theorem for image. (Contributed by FL, 15-Dec-2006.) |
Theorem | imaeq12d 5467 | Equality theorem for image. (Contributed by Mario Carneiro, 4-Dec-2016.) |
Theorem | dfima2 5468* | Alternate definition of image. Compare definition (d) of [Enderton] p. 44. (Contributed by NM, 19-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | dfima3 5469* | Alternate definition of image. Compare definition (d) of [Enderton] p. 44. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | elimag 5470* | Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 20-Jan-2007.) |
Theorem | elima 5471* | Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 19-Apr-2004.) |
Theorem | elima2 5472* | Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 11-Aug-2004.) |
Theorem | elima3 5473* | Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 14-Aug-1994.) |
Theorem | nfima 5474 | Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | nfimad 5475 | Deduction version of bound-variable hypothesis builder nfima 5474. (Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | imadmrn 5476 | The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994.) |
Theorem | imassrn 5477 | The image of a class is a subset of its range. Theorem 3.16(xi) of [Monk1] p. 39. (Contributed by NM, 31-Mar-1995.) |
Theorem | imai 5478 | Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38. (Contributed by NM, 30-Apr-1998.) |
Theorem | rnresi 5479 | The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.) |
Theorem | resiima 5480 | The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006.) |
Theorem | ima0 5481 | Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.) |
Theorem | 0ima 5482 | Image under the empty relation. (Contributed by FL, 11-Jan-2007.) |
Theorem | csbima12 5483 | Move class substitution in and out of the image of a function. (Contributed by FL, 15-Dec-2006.) (Revised by NM, 20-Aug-2018.) |
Theorem | imadisj 5484 | A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007.) |
Theorem | cnvimass 5485 | A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.) |
Theorem | cnvimarndm 5486 | The preimage of the range of a class is the domain of the class. (Contributed by Jeff Hankins, 15-Jul-2009.) |
Theorem | imasng 5487* | The image of a singleton. (Contributed by NM, 8-May-2005.) |
Theorem | relimasn 5488* | The image of a singleton. (Contributed by NM, 20-May-1998.) |
Theorem | elrelimasn 5489 | Elementhood in the image of a singleton. (Contributed by Mario Carneiro, 3-Nov-2015.) |
Theorem | elimasn 5490 | Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | elimasng 5491 | Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.) |
Theorem | elimasni 5492 | Membership in an image of a singleton. (Contributed by NM, 5-Aug-2010.) |
Theorem | args 5493* | Two ways to express the class of unique-valued arguments of , which is the same as the domain of whenever is a function. The left-hand side of the equality is from Definition 10.2 of [Quine] p. 65. Quine uses the notation "arg " for this class (for which we have no separate notation). Observe the resemblance to the alternate definition dffv4 6188 of function value, which is based on the idea in Quine's definition. (Contributed by NM, 8-May-2005.) |
Theorem | eliniseg 5494 | Membership in an initial segment. The idiom , meaning , is used to specify an initial segment in (for example) Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 28-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | epini 5495 | Any set is equal to its preimage under the converse epsilon relation. (Contributed by Mario Carneiro, 9-Mar-2013.) |
Theorem | iniseg 5496* | An idiom that signifies an initial segment of an ordering, used, for example, in Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 28-Apr-2004.) |
Theorem | inisegn0 5497 | Nonemptiness of an initial segment in terms of range. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
Theorem | dffr3 5498* | Alternate definition of well-founded relation. Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 23-Apr-2004.) (Revised by Mario Carneiro, 23-Jun-2015.) |
Theorem | dfse2 5499* | Alternate definition of set-like relation. (Contributed by Mario Carneiro, 23-Jun-2015.) |
Se | ||
Theorem | imass1 5500 | Subset theorem for image. (Contributed by NM, 16-Mar-2004.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |