Home | Metamath
Proof Explorer Theorem List (p. 54 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 | nfcnv 5301 | Bound-variable hypothesis builder for converse. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | opelcnvg 5302 | Ordered-pair membership in converse. (Contributed by NM, 13-May-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | brcnvg 5303 | The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.) |
Theorem | opelcnv 5304 | Ordered-pair membership in converse. (Contributed by NM, 13-Aug-1995.) |
Theorem | brcnv 5305 | The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.) |
Theorem | csbcnv 5306 | Move class substitution in and out of the converse of a function. Version of csbcnvgALT 5307 without a sethood antecedent but depending on more axioms. (Contributed by Thierry Arnoux, 8-Feb-2017.) (Revised by NM, 23-Aug-2018.) |
Theorem | csbcnvgALT 5307 | Move class substitution in and out of the converse of a function. Version of csbcnv 5306 with a sethood antecedent but depending on fewer axioms. (Contributed by Thierry Arnoux, 8-Feb-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | cnvco 5308 | Distributive law of converse over class composition. Theorem 26 of [Suppes] p. 64. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | cnvuni 5309* | The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.) |
Theorem | dfdm3 5310* | Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.) |
Theorem | dfrn2 5311* | Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.) |
Theorem | dfrn3 5312* | Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.) |
Theorem | elrn2g 5313* | Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.) |
Theorem | elrng 5314* | Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.) |
Theorem | ssrelrn 5315* | If a relation is a subset of a cartesian product, then for each element of the range of the relation there is an element of the first set of the cartesian product which is related to the element of the range by the relation. (Contributed by AV, 24-Oct-2020.) |
Theorem | dfdm4 5316 | Alternate definition of domain. (Contributed by NM, 28-Dec-1996.) |
Theorem | dfdmf 5317* | Definition of domain, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | csbdm 5318 | Distribute proper substitution through the domain of a class. (Contributed by Alexander van der Vekens, 23-Jul-2017.) (Revised by NM, 24-Aug-2018.) |
Theorem | eldmg 5319* | Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.) |
Theorem | eldm2g 5320* | Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.) |
Theorem | eldm 5321* | Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.) |
Theorem | eldm2 5322* | Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.) |
Theorem | dmss 5323 | Subset theorem for domain. (Contributed by NM, 11-Aug-1994.) |
Theorem | dmeq 5324 | Equality theorem for domain. (Contributed by NM, 11-Aug-1994.) |
Theorem | dmeqi 5325 | Equality inference for domain. (Contributed by NM, 4-Mar-2004.) |
Theorem | dmeqd 5326 | Equality deduction for domain. (Contributed by NM, 4-Mar-2004.) |
Theorem | opeldmd 5327 | Membership of first of an ordered pair in a domain. Deduction version of opeldm 5328. (Contributed by AV, 11-Mar-2021.) |
Theorem | opeldm 5328 | Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.) |
Theorem | breldm 5329 | Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.) |
Theorem | breldmg 5330 | Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.) |
Theorem | dmun 5331 | The domain of a union is the union of domains. Exercise 56(a) of [Enderton] p. 65. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | dmin 5332 | The domain of an intersection belong to the intersection of domains. Theorem 6 of [Suppes] p. 60. (Contributed by NM, 15-Sep-2004.) |
Theorem | dmiun 5333 | The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016.) |
Theorem | dmuni 5334* | The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 3-Feb-2004.) |
Theorem | dmopab 5335* | The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.) |
Theorem | dmopabss 5336* | Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.) |
Theorem | dmopab3 5337* | The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.) |
Theorem | opabssxpd 5338* | An ordered-pair class abstraction is a subset of an Cartesian product. Formerly part of proof for opabex2 7227. (Contributed by AV, 26-Nov-2021.) |
Theorem | dm0 5339 | The domain of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] p. 36. (Contributed by NM, 4-Jul-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | dmi 5340 | The domain of the identity relation is the universe. (Contributed by NM, 30-Apr-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | dmv 5341 | The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.) |
Theorem | dm0rn0 5342 | An empty domain is equivalent to an empty range. (Contributed by NM, 21-May-1998.) |
Theorem | reldm0 5343 | A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.) |
Theorem | dmxp 5344 | The domain of a Cartesian product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | dmxpid 5345 | The domain of a square Cartesian product. (Contributed by NM, 28-Jul-1995.) |
Theorem | dmxpin 5346 | The domain of the intersection of two square Cartesian products. Unlike dmin 5332, equality holds. (Contributed by NM, 29-Jan-2008.) |
Theorem | xpid11 5347 | The Cartesian product of a class with itself is one-to-one. (Contributed by NM, 5-Nov-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | dmcnvcnv 5348 | The domain of the double converse of a class (which doesn't have to be a relation as in dfrel2 5583). (Contributed by NM, 8-Apr-2007.) |
Theorem | rncnvcnv 5349 | The range of the double converse of a class. (Contributed by NM, 8-Apr-2007.) |
Theorem | elreldm 5350 | The first member of an ordered pair in a relation belongs to the domain of the relation. (Contributed by NM, 28-Jul-2004.) |
Theorem | rneq 5351 | Equality theorem for range. (Contributed by NM, 29-Dec-1996.) |
Theorem | rneqi 5352 | Equality inference for range. (Contributed by NM, 4-Mar-2004.) |
Theorem | rneqd 5353 | Equality deduction for range. (Contributed by NM, 4-Mar-2004.) |
Theorem | rnss 5354 | Subset theorem for range. (Contributed by NM, 22-Mar-1998.) |
Theorem | brelrng 5355 | The second argument of a binary relation belongs to its range. (Contributed by NM, 29-Jun-2008.) |
Theorem | brelrn 5356 | The second argument of a binary relation belongs to its range. (Contributed by NM, 13-Aug-2004.) |
Theorem | opelrn 5357 | Membership of second member of an ordered pair in a range. (Contributed by NM, 23-Feb-1997.) |
Theorem | releldm 5358 | The first argument of a binary relation belongs to its domain. Note that does not imply : see for example nrelv 5244 and brv 4941. (Contributed by NM, 2-Jul-2008.) |
Theorem | relelrn 5359 | The second argument of a binary relation belongs to its range. (Contributed by NM, 2-Jul-2008.) |
Theorem | releldmb 5360* | Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.) |
Theorem | relelrnb 5361* | Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.) |
Theorem | releldmi 5362 | The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.) |
Theorem | relelrni 5363 | The second argument of a binary relation belongs to its range. (Contributed by NM, 28-Apr-2015.) |
Theorem | dfrnf 5364* | Definition of range, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Aug-1995.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | elrn2 5365* | Membership in a range. (Contributed by NM, 10-Jul-1994.) |
Theorem | elrn 5366* | Membership in a range. (Contributed by NM, 2-Apr-2004.) |
Theorem | nfdm 5367 | Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | nfrn 5368 | Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | dmiin 5369 | Domain of an intersection. (Contributed by FL, 15-Oct-2012.) |
Theorem | rnopab 5370* | The range of a class of ordered pairs. (Contributed by NM, 14-Aug-1995.) (Revised by Mario Carneiro, 4-Dec-2016.) |
Theorem | rnmpt 5371* | The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | elrnmpt 5372* | The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015.) |
Theorem | elrnmpt1s 5373* | Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015.) |
Theorem | elrnmpt1 5374 | Elementhood in an image set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
Theorem | elrnmptg 5375* | Membership in the range of a function. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | elrnmpti 5376* | Membership in the range of a function. (Contributed by NM, 30-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | rn0 5377 | The range of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] p. 36. (Contributed by NM, 4-Jul-1994.) |
Theorem | dfiun3g 5378 | Alternate definition of indexed union when is a set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
Theorem | dfiin3g 5379 | Alternate definition of indexed intersection when is a set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
Theorem | dfiun3 5380 | Alternate definition of indexed union when is a set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
Theorem | dfiin3 5381 | Alternate definition of indexed intersection when is a set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
Theorem | riinint 5382* | Express a relative indexed intersection as an intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
Theorem | relrn0 5383 | A relation is empty iff its range is empty. (Contributed by NM, 15-Sep-2004.) |
Theorem | dmrnssfld 5384 | The domain and range of a class are included in its double union. (Contributed by NM, 13-May-2008.) |
Theorem | dmcoss 5385 | Domain of a composition. Theorem 21 of [Suppes] p. 63. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | rncoss 5386 | Range of a composition. (Contributed by NM, 19-Mar-1998.) |
Theorem | dmcosseq 5387 | Domain of a composition. (Contributed by NM, 28-May-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | dmcoeq 5388 | Domain of a composition. (Contributed by NM, 19-Mar-1998.) |
Theorem | rncoeq 5389 | Range of a composition. (Contributed by NM, 19-Mar-1998.) |
Theorem | reseq1 5390 | Equality theorem for restrictions. (Contributed by NM, 7-Aug-1994.) |
Theorem | reseq2 5391 | Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.) |
Theorem | reseq1i 5392 | Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.) |
Theorem | reseq2i 5393 | Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | reseq12i 5394 | Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.) |
Theorem | reseq1d 5395 | Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.) |
Theorem | reseq2d 5396 | Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | reseq12d 5397 | Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.) |
Theorem | nfres 5398 | Bound-variable hypothesis builder for restriction. (Contributed by NM, 15-Sep-2003.) (Revised by David Abernethy, 19-Jun-2012.) |
Theorem | csbres 5399 | Distribute proper substitution through the restriction of a class. (Contributed by Alan Sare, 10-Nov-2012.) (Revised by NM, 23-Aug-2018.) |
Theorem | res0 5400 | A restriction to the empty set is empty. (Contributed by NM, 12-Nov-1994.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |