Home | Metamath
Proof Explorer Theorem List (p. 32 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 | rexcom13 3101* | Swap first and third restricted existential quantifiers. (Contributed by NM, 8-Apr-2015.) |
Theorem | ralrot3 3102* | Rotate three restricted universal quantifiers. (Contributed by AV, 3-Dec-2021.) |
Theorem | rexrot4 3103* | Rotate four restricted existential quantifiers twice. (Contributed by NM, 8-Apr-2015.) |
Theorem | ralcom2 3104* | Commutation of restricted universal quantifiers. Note that and need not be disjoint (this makes the proof longer). If and are disjoint, then one may use ralcom 3098. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) |
Theorem | ralcom3 3105 | A commutation law for restricted universal quantifiers that swaps the domains of the restriction. (Contributed by NM, 22-Feb-2004.) |
Theorem | reean 3106* | Rearrange restricted existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
Theorem | reeanv 3107* | Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999.) |
Theorem | 3reeanv 3108* | Rearrange three restricted existential quantifiers. (Contributed by Jeff Madsen, 11-Jun-2010.) |
Theorem | 2ralor 3109* | Distribute restricted universal quantification over "or". (Contributed by Jeff Madsen, 19-Jun-2010.) |
Theorem | nfreu1 3110 | The setvar is not free in . (Contributed by NM, 19-Mar-1997.) |
Theorem | nfrmo1 3111 | The setvar is not free in . (Contributed by NM, 16-Jun-2017.) |
Theorem | nfreud 3112 | Deduction version of nfreu 3114. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 8-Oct-2016.) |
Theorem | nfrmod 3113 | Deduction version of nfrmo 3115. (Contributed by NM, 17-Jun-2017.) |
Theorem | nfreu 3114 | Bound-variable hypothesis builder for restricted unique existence. (Contributed by NM, 30-Oct-2010.) (Revised by Mario Carneiro, 8-Oct-2016.) |
Theorem | nfrmo 3115 | Bound-variable hypothesis builder for restricted uniqueness. (Contributed by NM, 16-Jun-2017.) |
Theorem | rabid 3116 | An "identity" law of concretion for restricted abstraction. Special case of Definition 2.1 of [Quine] p. 16. (Contributed by NM, 9-Oct-2003.) |
Theorem | rabidim1 3117 | Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | rabid2 3118* | An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
Theorem | rabid2f 3119 | An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.) |
Theorem | rabbi 3120 | Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbidva 3188. (Contributed by NM, 25-Nov-2013.) |
Theorem | rabswap 3121 | Swap with a membership relation in a restricted class abstraction. (Contributed by NM, 4-Jul-2005.) |
Theorem | nfrab1 3122 | The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997.) |
Theorem | nfrab 3123 | A variable not free in a wff remains so in a restricted class abstraction. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.) |
Theorem | reubida 3124 | Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by Mario Carneiro, 19-Nov-2016.) |
Theorem | reubidva 3125* | Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 13-Nov-2004.) |
Theorem | reubidv 3126* | Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 17-Oct-1996.) |
Theorem | reubiia 3127 | Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 14-Nov-2004.) |
Theorem | reubii 3128 | Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 22-Oct-1999.) |
Theorem | rmobida 3129 | Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.) |
Theorem | rmobidva 3130* | Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.) |
Theorem | rmobidv 3131* | Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.) |
Theorem | rmobiia 3132 | Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 16-Jun-2017.) |
Theorem | rmobii 3133 | Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 16-Jun-2017.) |
Theorem | raleqf 3134 | Equality theorem for restricted universal quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004.) (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | rexeqf 3135 | Equality theorem for restricted existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 9-Oct-2003.) (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | reueq1f 3136 | Equality theorem for restricted uniqueness quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 5-Apr-2004.) (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | rmoeq1f 3137 | Equality theorem for restricted uniqueness quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | raleq 3138* | Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) |
Theorem | rexeq 3139* | Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) |
Theorem | reueq1 3140* | Equality theorem for restricted uniqueness quantifier. (Contributed by NM, 5-Apr-2004.) |
Theorem | rmoeq1 3141* | Equality theorem for restricted uniqueness quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | raleqi 3142* | Equality inference for restricted universal qualifier. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | rexeqi 3143* | Equality inference for restricted existential qualifier. (Contributed by Mario Carneiro, 23-Apr-2015.) |
Theorem | raleqdv 3144* | Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.) |
Theorem | rexeqdv 3145* | Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.) |
Theorem | raleqbi1dv 3146* | Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) |
Theorem | rexeqbi1dv 3147* | Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.) |
Theorem | reueqd 3148* | Equality deduction for restricted uniqueness quantifier. (Contributed by NM, 5-Apr-2004.) |
Theorem | rmoeqd 3149* | Equality deduction for restricted uniqueness quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | raleqbid 3150 | Equality deduction for restricted universal quantifier. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
Theorem | rexeqbid 3151 | Equality deduction for restricted existential quantifier. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
Theorem | raleqbidv 3152* | Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) |
Theorem | rexeqbidv 3153* | Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) |
Theorem | raleqbidva 3154* | Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.) |
Theorem | rexeqbidva 3155* | Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.) |
Theorem | raleleq 3156* | All elements of a class are elements of a class equal to this class. (Contributed by AV, 30-Oct-2020.) |
Theorem | raleleqALT 3157* | Alternate proof of raleleq 3156 using ralel 2923, being longer and using more axioms. (Contributed by AV, 30-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | mormo 3158 | Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.) |
Theorem | reu5 3159 | Restricted uniqueness in terms of "at most one." (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.) |
Theorem | reurex 3160 | Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.) |
Theorem | reurmo 3161 | Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.) |
Theorem | rmo5 3162 | Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017.) |
Theorem | nrexrmo 3163 | Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.) |
Theorem | reueubd 3164* | Restricted existential uniqueness is equivalent with existential uniqueness if the unique element is in the restricting class. (Contributed by AV, 4-Jan-2021.) |
Theorem | cbvralf 3165 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 7-Mar-2004.) (Revised by Mario Carneiro, 9-Oct-2016.) |
Theorem | cbvrexf 3166 | Rule used to change bound variables, using implicit substitution. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 9-Oct-2016.) |
Theorem | cbvral 3167* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.) |
Theorem | cbvrex 3168* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | cbvreu 3169* | Change the bound variable of a restricted uniqueness quantifier using implicit substitution. (Contributed by Mario Carneiro, 15-Oct-2016.) |
Theorem | cbvrmo 3170* | Change the bound variable of restricted "at most one" using implicit substitution. (Contributed by NM, 16-Jun-2017.) |
Theorem | cbvralv 3171* | Change the bound variable of a restricted universal quantifier using implicit substitution. (Contributed by NM, 28-Jan-1997.) |
Theorem | cbvrexv 3172* | Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.) |
Theorem | cbvreuv 3173* | Change the bound variable of a restricted uniqueness quantifier using implicit substitution. (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | cbvrmov 3174* | Change the bound variable of a restricted uniqueness quantifier using implicit substitution. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | cbvraldva2 3175* | Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017.) |
Theorem | cbvrexdva2 3176* | Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017.) |
Theorem | cbvraldva 3177* | Rule used to change the bound variable in a restricted universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) |
Theorem | cbvrexdva 3178* | Rule used to change the bound variable in a restricted existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) |
Theorem | cbvral2v 3179* | Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by NM, 10-Aug-2004.) |
Theorem | cbvrex2v 3180* | Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by FL, 2-Jul-2012.) |
Theorem | cbvral3v 3181* | Change bound variables of triple restricted universal quantification, using implicit substitution. (Contributed by NM, 10-May-2005.) |
Theorem | cbvralsv 3182* | Change bound variable by using a substitution. (Contributed by NM, 20-Nov-2005.) (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | cbvrexsv 3183* | Change bound variable by using a substitution. (Contributed by NM, 2-Mar-2008.) (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | sbralie 3184* | Implicit to explicit substitution that swaps variables in a quantified expression. (Contributed by NM, 5-Sep-2004.) |
Theorem | rabbiia 3185 | Equivalent wff's yield equal restricted class abstractions (inference rule). (Contributed by NM, 22-May-1999.) |
Theorem | rabbidva2 3186* | Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
Theorem | rabbia2 3187 | Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | rabbidva 3188* | Equivalent wff's yield equal restricted class abstractions (deduction rule). (Contributed by NM, 28-Nov-2003.) |
Theorem | rabbidv 3189* | Equivalent wff's yield equal restricted class abstractions (deduction rule). (Contributed by NM, 10-Feb-1995.) |
Theorem | rabeqf 3190 | Equality theorem for restricted class abstractions, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004.) |
Theorem | rabeqif 3191 | Equality theorem for restricted class abstractions. Inference form of rabeqf 3190. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | rabeq 3192* | Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) |
Theorem | rabeqi 3193* | Equality theorem for restricted class abstractions. Inference form of rabeq 3192. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | rabeqdv 3194* | Equality of restricted class abstractions. Deduction form of rabeq 3192. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
Theorem | rabeqbidv 3195* | Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.) |
Theorem | rabeqbidva 3196* | Equality of restricted class abstractions. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Theorem | rabeq2i 3197 | Inference rule from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.) |
Theorem | cbvrab 3198 | Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 9-Oct-2016.) |
Theorem | cbvrabv 3199* | Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.) |
Syntax | cvv 3200 | Extend class notation to include the universal class symbol. |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |