Home | Metamath
Proof Explorer Theorem List (p. 43 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 | nelpri 4201 | If an element doesn't match the items in an unordered pair, it is not in the unordered pair. (Contributed by David A. Wheeler, 10-May-2015.) |
Theorem | prneli 4202 | If an element doesn't match the items in an unordered pair, it is not in the unordered pair, using . (Contributed by David A. Wheeler, 10-May-2015.) |
Theorem | nelprd 4203 | If an element doesn't match the items in an unordered pair, it is not in the unordered pair, deduction version. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
Theorem | eldifpr 4204 | Membership in a set with two elements removed. Similar to eldifsn 4317 and eldiftp 4228. (Contributed by Mario Carneiro, 18-Jul-2017.) |
Theorem | rexdifpr 4205 | Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018.) |
Theorem | snidg 4206 | A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 28-Oct-2003.) |
Theorem | snidb 4207 | A class is a set iff it is a member of its singleton. (Contributed by NM, 5-Apr-2004.) |
Theorem | snid 4208 | A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.) |
Theorem | vsnid 4209 | A setvar variable is a member of its singleton (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | elsn2g 4210 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that , rather than , be a set. (Contributed by NM, 28-Oct-2003.) |
Theorem | elsn2 4211 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that , rather than , be a set. (Contributed by NM, 12-Jun-1994.) |
Theorem | nelsn 4212 | If a class is not equal to the class in a singleton, then it is not in the singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof shortened by BJ, 4-May-2021.) |
Theorem | nelsnOLD 4213 | Obsolete proof of nelsn 4212 as of 4-May-2021. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | rabeqsn 4214* | Conditions for a restricted class abstraction to be a singleton. (Contributed by AV, 18-Apr-2019.) |
Theorem | rabsssn 4215* | Conditions for a restricted class abstraction to be a subset of a singleton, i.e. to be a singleton or the empty set. (Contributed by AV, 18-Apr-2019.) |
Theorem | ralsnsg 4216* | Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) |
Theorem | rexsns 4217* | Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by NM, 22-Aug-2018.) |
Theorem | ralsng 4218* | Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) |
Theorem | rexsng 4219* | Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) |
Theorem | 2ralsng 4220* | Substitution expressed in terms of two quantifications over singletons. (Contributed by AV, 22-Dec-2019.) |
Theorem | exsnrex 4221 | There is a set being the element of a singleton if and only if there is an element of the singleton. (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
Theorem | ralsn 4222* | Convert a quantification over a singleton to a substitution. (Contributed by NM, 27-Apr-2009.) |
Theorem | rexsn 4223* | Restricted existential quantification over a singleton. (Contributed by Jeff Madsen, 5-Jan-2011.) |
Theorem | elpwunsn 4224 | Membership in an extension of a power class. (Contributed by NM, 26-Mar-2007.) |
Theorem | eqoreldif 4225 | An element of a set is either equal to another element of the set or a member of the difference of the set and the singleton containing the other element. (Contributed by AV, 25-Aug-2020.) (Proof shortened by JJ, 23-Jul-2021.) |
Theorem | eqoreldifOLD 4226 | Obsolete proof of eqoreldif 4225 as of 23-Jul-2021. (Contributed by AV, 25-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | eltpg 4227 | Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.) |
Theorem | eldiftp 4228 | Membership in a set with three elements removed. Similar to eldifsn 4317 and eldifpr 4204. (Contributed by David A. Wheeler, 22-Jul-2017.) |
Theorem | eltpi 4229 | A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.) |
Theorem | eltp 4230 | A member of an unordered triple of classes is one of them. Special case of Exercise 1 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Apr-1994.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Theorem | dftp2 4231* | Alternate definition of unordered triple of classes. Special case of Definition 5.3 of [TakeutiZaring] p. 16. (Contributed by NM, 8-Apr-1994.) |
Theorem | nfpr 4232 | Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.) |
Theorem | ifpr 4233 | Membership of a conditional operator in an unordered pair. (Contributed by NM, 17-Jun-2007.) |
Theorem | ralprg 4234* | Convert a quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) |
Theorem | rexprg 4235* | Convert a quantification over a pair to a disjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) |
Theorem | raltpg 4236* | Convert a quantification over a triple to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) |
Theorem | rextpg 4237* | Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.) |
Theorem | ralpr 4238* | Convert a quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.) |
Theorem | rexpr 4239* | Convert an existential quantification over a pair to a disjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.) |
Theorem | raltp 4240* | Convert a quantification over a triple to a conjunction. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) |
Theorem | rextp 4241* | Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.) |
Theorem | nfsn 4242 | Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.) |
Theorem | csbsng 4243 | Distribute proper substitution through the singleton of a class. csbsng 4243 is derived from the virtual deduction proof csbsngVD 39129. (Contributed by Alan Sare, 10-Nov-2012.) |
Theorem | csbprg 4244 | Distribute proper substitution through a pair of classes. (Contributed by Alexander van der Vekens, 4-Sep-2018.) |
Theorem | elinsn 4245 | If the intersection of two classes is a (proper) singleton, then the singleton element is a member of both classes. (Contributed by AV, 30-Dec-2021.) |
Theorem | disjsn 4246 | Intersection with the singleton of a non-member is disjoint. (Contributed by NM, 22-May-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.) |
Theorem | disjsn2 4247 | Two distinct singletons are disjoint. (Contributed by NM, 25-May-1998.) |
Theorem | disjpr2 4248 | Two completely distinct unordered pairs are disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Proof shortened by JJ, 23-Jul-2021.) |
Theorem | disjpr2OLD 4249 | Obsolete proof of disjpr2 4248 as of 23-Jul-2021. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | disjprsn 4250 | The disjoint intersection of an unordered pair and a singleton. (Contributed by AV, 23-Jan-2021.) |
Theorem | disjtpsn 4251 | The disjoint intersection of an unordered triple and a singleton. (Contributed by AV, 14-Nov-2021.) |
Theorem | disjtp2 4252 | Two completely distinct unordered triples are disjoint. (Contributed by AV, 14-Nov-2021.) |
Theorem | snprc 4253 | The singleton of a proper class (one that doesn't exist) is the empty set. Theorem 7.2 of [Quine] p. 48. (Contributed by NM, 21-Jun-1993.) |
Theorem | snnzb 4254 | A singleton is nonempty iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018.) |
Theorem | r19.12sn 4255* | Special case of r19.12 3063 where its converse holds. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.) (Revised by BJ, 18-Mar-2020.) |
Theorem | rabsn 4256* | Condition where a restricted class abstraction is a singleton. (Contributed by NM, 28-May-2006.) |
Theorem | rabsnifsb 4257* | A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 21-Jul-2019.) |
Theorem | rabsnif 4258* | A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 21-Jul-2019.) |
Theorem | rabrsn 4259* | A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by Alexander van der Vekens, 22-Dec-2017.) (Proof shortened by AV, 21-Jul-2019.) |
Theorem | euabsn2 4260* | Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016.) |
Theorem | euabsn 4261 | Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004.) |
Theorem | reusn 4262* | A way to express restricted existential uniqueness of a wff: its restricted class abstraction is a singleton. (Contributed by NM, 30-May-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.) |
Theorem | absneu 4263 | Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) |
Theorem | rabsneu 4264 | Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro, 23-Dec-2016.) |
Theorem | eusn 4265* | Two ways to express " is a singleton." (Contributed by NM, 30-Oct-2010.) |
Theorem | rabsnt 4266* | Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by NM, 29-May-2006.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
Theorem | prcom 4267 | Commutative law for unordered pairs. (Contributed by NM, 15-Jul-1993.) |
Theorem | preq1 4268 | Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.) |
Theorem | preq2 4269 | Equality theorem for unordered pairs. (Contributed by NM, 15-Jul-1993.) |
Theorem | preq12 4270 | Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
Theorem | preq1i 4271 | Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
Theorem | preq2i 4272 | Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
Theorem | preq12i 4273 | Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
Theorem | preq1d 4274 | Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
Theorem | preq2d 4275 | Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
Theorem | preq12d 4276 | Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
Theorem | tpeq1 4277 | Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.) |
Theorem | tpeq2 4278 | Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.) |
Theorem | tpeq3 4279 | Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.) |
Theorem | tpeq1d 4280 | Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.) |
Theorem | tpeq2d 4281 | Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.) |
Theorem | tpeq3d 4282 | Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.) |
Theorem | tpeq123d 4283 | Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.) |
Theorem | tprot 4284 | Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.) |
Theorem | tpcoma 4285 | Swap 1st and 2nd members of an unordered triple. (Contributed by NM, 22-May-2015.) |
Theorem | tpcomb 4286 | Swap 2nd and 3rd members of an unordered triple. (Contributed by NM, 22-May-2015.) |
Theorem | tpass 4287 | Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
Theorem | qdass 4288 | Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
Theorem | qdassr 4289 | Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
Theorem | tpidm12 4290 | Unordered triple is just an overlong way to write . (Contributed by David A. Wheeler, 10-May-2015.) |
Theorem | tpidm13 4291 | Unordered triple is just an overlong way to write . (Contributed by David A. Wheeler, 10-May-2015.) |
Theorem | tpidm23 4292 | Unordered triple is just an overlong way to write . (Contributed by David A. Wheeler, 10-May-2015.) |
Theorem | tpidm 4293 | Unordered triple is just an overlong way to write . (Contributed by David A. Wheeler, 10-May-2015.) |
Theorem | tppreq3 4294 | An unordered triple is an unordered pair if one of its elements is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
Theorem | prid1g 4295 | An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.) |
Theorem | prid2g 4296 | An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.) |
Theorem | prid1 4297 | An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 24-Jun-1993.) |
Theorem | prid2 4298 | An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.) |
Theorem | ifpprsnss 4299 | An unordered pair is a singleton or a subset of itself. This theorem is helpful to convert theorems about walks in arbitrary graphs into theorems about walks in pseudographs. (Contributed by AV, 27-Feb-2021.) |
if- | ||
Theorem | prprc1 4300 | A proper class vanishes in an unordered pair. (Contributed by NM, 15-Jul-1993.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |