Home | Metamath
Proof Explorer Theorem List (p. 33 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 | vjust 3201 | Soundness justification theorem for df-v 3202. (Contributed by Rodolfo Medina, 27-Apr-2010.) |
Definition | df-v 3202 | Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21. Also Definition 2.9 of [Quine] p. 19. The class can be described as the "class of all sets"; vprc 4796 proves that is not itself a set in ZFC. We will frequently use the expression as a short way to say " is a set", and isset 3207 proves that this expression has the same meaning as . The class is called the "von Neumann universe", however, the letter "V" is not a tribute to the name of von Neumann. The letter "V" was used earlier by Peano in 1889 for the universe of sets, where the letter V is derived from the word "Verum". Peano's notation V was adopted by Whitehead and Russell in Principia Mathematica for the class of all sets in 1910. For a general discussion of the theory of classes, see mmset.html#class. (Contributed by NM, 26-May-1993.) |
Theorem | vex 3203 | All setvar variables are sets (see isset 3207). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 26-May-1993.) |
Theorem | eqvf 3204 | The universe contains every set. (Contributed by BJ, 15-Jul-2021.) |
Theorem | eqv 3205* | The universe contains every set. (Contributed by NM, 11-Sep-2006.) |
Theorem | abv 3206 | The class of sets verifying a property is the universal class if and only if that property is a tautology. (Contributed by BJ, 19-Mar-2021.) |
Theorem | isset 3207* |
Two ways to say "
is a set": A class is a member of the
universal class (see df-v 3202) if and only if the class
exists (i.e. there exists some set equal to class ).
Theorem 6.9 of [Quine] p. 43.
Notational convention: We will use the
notational device " " to mean
" is a set"
very
frequently, for example in uniex 6953. Note the when is not a set,
it is called a proper class. In some theorems, such as uniexg 6955, in
order to shorten certain proofs we use the more general antecedent
instead of to
mean " is a
set."
Note that a constant is implicitly considered distinct from all variables. This is why is not included in the distinct variable list, even though df-clel 2618 requires that the expression substituted for not contain . (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 26-May-1993.) |
Theorem | issetf 3208 | A version of isset 3207 that does not require and to be distinct. (Contributed by Andrew Salmon, 6-Jun-2011.) (Revised by Mario Carneiro, 10-Oct-2016.) |
Theorem | isseti 3209* | A way to say " is a set" (inference rule). (Contributed by NM, 24-Jun-1993.) |
Theorem | issetri 3210* | A way to say " is a set" (inference rule). (Contributed by NM, 21-Jun-1993.) |
Theorem | eqvisset 3211 | A class equal to a variable is a set. Note the absence of dv condition, contrary to isset 3207 and issetri 3210. (Contributed by BJ, 27-Apr-2019.) |
Theorem | elex 3212 | If a class is a member of another class, it is a set. Theorem 6.12 of [Quine] p. 44. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | elexi 3213 | If a class is a member of another class, it is a set. (Contributed by NM, 11-Jun-1994.) |
Theorem | elexd 3214 | If a class is a member of another class, it is a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Theorem | elisset 3215* | An element of a class exists. (Contributed by NM, 1-May-1995.) |
Theorem | elex2 3216* | If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.) |
Theorem | elex22 3217* | If two classes each contain another class, then both contain some set. (Contributed by Alan Sare, 24-Oct-2011.) |
Theorem | prcnel 3218 | A proper class doesn't belong to any class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof shortened by AV, 14-Nov-2020.) |
Theorem | ralv 3219 | A universal quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.) |
Theorem | rexv 3220 | An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.) |
Theorem | reuv 3221 | A uniqueness quantifier restricted to the universe is unrestricted. (Contributed by NM, 1-Nov-2010.) |
Theorem | rmov 3222 | A uniqueness quantifier restricted to the universe is unrestricted. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | rabab 3223 | A class abstraction restricted to the universe is unrestricted. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | ralcom4 3224* | Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | rexcom4 3225* | Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | rexcom4a 3226* | Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.) |
Theorem | rexcom4b 3227* | Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.) |
Theorem | ceqsalt 3228* | Closed theorem version of ceqsalg 3230. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.) |
Theorem | ceqsralt 3229* | Restricted quantifier version of ceqsalt 3228. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.) |
Theorem | ceqsalg 3230* | A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. For an alternate proof, see ceqsalgALT 3231. (Contributed by NM, 29-Oct-2003.) (Proof shortened by BJ, 29-Sep-2019.) |
Theorem | ceqsalgALT 3231* | Alternate proof of ceqsalg 3230, not using ceqsalt 3228. (Contributed by NM, 29-Oct-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Revised by BJ, 29-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ceqsal 3232* | A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.) |
Theorem | ceqsalv 3233* | A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.) |
Theorem | ceqsralv 3234* | Restricted quantifier version of ceqsalv 3233. (Contributed by NM, 21-Jun-2013.) |
Theorem | gencl 3235* | Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.) |
Theorem | 2gencl 3236* | Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.) |
Theorem | 3gencl 3237* | Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.) |
Theorem | cgsexg 3238* | Implicit substitution inference for general classes. (Contributed by NM, 26-Aug-2007.) |
Theorem | cgsex2g 3239* | Implicit substitution inference for general classes. (Contributed by NM, 26-Jul-1995.) |
Theorem | cgsex4g 3240* | An implicit substitution inference for 4 general classes. (Contributed by NM, 5-Aug-1995.) |
Theorem | ceqsex 3241* | Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) (Revised by Mario Carneiro, 10-Oct-2016.) |
Theorem | ceqsexv 3242* | Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) |
Theorem | ceqsexv2d 3243* | Elimination of an existential quantifier, using implicit substitution. (Contributed by Thierry Arnoux, 10-Sep-2016.) |
Theorem | ceqsex2 3244* | Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.) |
Theorem | ceqsex2v 3245* | Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.) |
Theorem | ceqsex3v 3246* | Elimination of three existential quantifiers, using implicit substitution. (Contributed by NM, 16-Aug-2011.) |
Theorem | ceqsex4v 3247* | Elimination of four existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.) |
Theorem | ceqsex6v 3248* | Elimination of six existential quantifiers, using implicit substitution. (Contributed by NM, 21-Sep-2011.) |
Theorem | ceqsex8v 3249* | Elimination of eight existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.) |
Theorem | gencbvex 3250* | Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | gencbvex2 3251* | Restatement of gencbvex 3250 with weaker hypotheses. (Contributed by Jeff Hankins, 6-Dec-2006.) |
Theorem | gencbval 3252* | Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.) |
Theorem | sbhypf 3253* | Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf 3552. (Contributed by Raph Levien, 10-Apr-2004.) |
Theorem | vtoclgft 3254 | Closed theorem form of vtoclgf 3264. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by JJ, 11-Aug-2021.) |
Theorem | vtoclgftOLD 3255 | Obsolete proof of vtoclgft 3254 as of 11-Aug-2021. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | vtocldf 3256 | Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.) |
Theorem | vtocld 3257* | Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.) |
Theorem | vtoclf 3258* | Implicit substitution of a class for a setvar variable. This is a generalization of chvar 2262. (Contributed by NM, 30-Aug-1993.) |
Theorem | vtocl 3259* | Implicit substitution of a class for a setvar variable. See also vtoclALT 3260. (Contributed by NM, 30-Aug-1993.) Removed dependency on ax-10 2019. (Revised by BJ, 29-Nov-2020.) |
Theorem | vtoclALT 3260* | Alternate proof of vtocl 3259. Shorter but requires more axioms. (Contributed by NM, 30-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | vtocl2 3261* | Implicit substitution of classes for setvar variables. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | vtocl3 3262* | Implicit substitution of classes for setvar variables. (Contributed by NM, 3-Jun-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | vtoclb 3263* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 23-Dec-1993.) |
Theorem | vtoclgf 3264 | Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint variable restrictions. (Contributed by NM, 21-Sep-2003.) (Proof shortened by Mario Carneiro, 10-Oct-2016.) |
Theorem | vtoclg1f 3265* | Version of vtoclgf 3264 with one non-freeness hypothesis replaced with a dv condition, thus avoiding dependency on ax-11 2034 and ax-13 2246. (Contributed by BJ, 1-May-2019.) |
Theorem | vtoclg 3266* | Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) |
Theorem | vtoclbg 3267* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.) |
Theorem | vtocl2gf 3268 | Implicit substitution of a class for a setvar variable. (Contributed by NM, 25-Apr-1995.) |
Theorem | vtocl3gf 3269 | Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 10-Oct-2016.) |
Theorem | vtocl2g 3270* | Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) |
Theorem | vtoclgaf 3271* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.) |
Theorem | vtoclga 3272* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.) |
Theorem | vtocl2gaf 3273* | Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 10-Aug-2013.) |
Theorem | vtocl2ga 3274* | Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.) |
Theorem | vtocl3gaf 3275* | Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 11-Oct-2016.) |
Theorem | vtocl3ga 3276* | Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 20-Aug-1995.) |
Theorem | vtocl4g 3277* | Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019.) |
Theorem | vtocl4ga 3278* | Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019.) |
Theorem | vtocleg 3279* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Jun-1993.) |
Theorem | vtoclegft 3280* | Implicit substitution of a class for a setvar variable. (Closed theorem version of vtoclef 3281.) (Contributed by NM, 7-Nov-2005.) (Revised by Mario Carneiro, 11-Oct-2016.) |
Theorem | vtoclef 3281* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 18-Aug-1993.) |
Theorem | vtocle 3282* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 9-Sep-1993.) |
Theorem | vtoclri 3283* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Nov-1994.) |
Theorem | spcimgft 3284 | A closed version of spcimgf 3286. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | spcgft 3285 | A closed version of spcgf 3288. (Contributed by Andrew Salmon, 6-Jun-2011.) (Revised by Mario Carneiro, 4-Jan-2017.) |
Theorem | spcimgf 3286 | Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | spcimegf 3287 | Existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | spcgf 3288 | Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 2-Feb-1997.) (Revised by Andrew Salmon, 12-Aug-2011.) |
Theorem | spcegf 3289 | Existential specialization, using implicit substitution. (Contributed by NM, 2-Feb-1997.) |
Theorem | spcimdv 3290* | Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | spcdv 3291* | Rule of specialization, using implicit substitution. Analogous to rspcdv 3312. (Contributed by David Moews, 1-May-2017.) |
Theorem | spcimedv 3292* | Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | spcgv 3293* | Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.) |
Theorem | spcegv 3294* | Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) |
Theorem | spc2egv 3295* | Existential specialization with two quantifiers, using implicit substitution. (Contributed by NM, 3-Aug-1995.) |
Theorem | spc2gv 3296* | Specialization with two quantifiers, using implicit substitution. (Contributed by NM, 27-Apr-2004.) |
Theorem | spc3egv 3297* | Existential specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.) |
Theorem | spc3gv 3298* | Specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.) |
Theorem | spcv 3299* | Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.) |
Theorem | spcev 3300* | Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |