Home | Intuitionistic Logic Explorer Theorem List (p. 28 of 138) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cbvrex2v 2701* | Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by FL, 2-Jul-2012.) |
Theorem | cbvral3v 2702* | Change bound variables of triple restricted universal quantification, using implicit substitution. (Contributed by NM, 10-May-2005.) |
Theorem | cbvralsv 2703* | Change bound variable by using a substitution. (Contributed by NM, 20-Nov-2005.) (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | cbvrexsv 2704* | Change bound variable by using a substitution. (Contributed by NM, 2-Mar-2008.) (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | sbralie 2705* | Implicit to explicit substitution that swaps variables in a quantified expression. (Contributed by NM, 5-Sep-2004.) |
Theorem | rabbiia 2706 | Equivalent wff's yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999.) |
Theorem | rabbii 2707 | Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 2710. (Contributed by Peter Mazsa, 1-Nov-2019.) |
Theorem | rabbidva2 2708* | Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
Theorem | rabbidva 2709* | Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.) |
Theorem | rabbidv 2710* | Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.) |
Theorem | rabeqf 2711 | Equality theorem for restricted class abstractions, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004.) |
Theorem | rabeqif 2712 | Equality theorem for restricted class abstractions. Inference form of rabeqf 2711. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | rabeq 2713* | Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) |
Theorem | rabeqi 2714* | Equality theorem for restricted class abstractions. Inference form of rabeq 2713. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | rabeqdv 2715* | Equality of restricted class abstractions. Deduction form of rabeq 2713. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
Theorem | rabeqbidv 2716* | Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.) |
Theorem | rabeqbidva 2717* | Equality of restricted class abstractions. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Theorem | rabeq2i 2718 | Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.) |
Theorem | cbvrab 2719 | 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 2720* | Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.) |
Syntax | cvv 2721 | Extend class notation to include the universal class symbol. |
Theorem | vjust 2722 | Soundness justification theorem for df-v 2723. (Contributed by Rodolfo Medina, 27-Apr-2010.) |
Definition | df-v 2723 | Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21. Also Definition 2.9 of [Quine] p. 19. (Contributed by NM, 5-Aug-1993.) |
Theorem | vex 2724 | All setvar variables are sets (see isset 2727). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.) |
Theorem | elv 2725 | Technical lemma used to shorten proofs. If a proposition is implied by (which is true, see vex 2724), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.) |
Theorem | elvd 2726 | Technical lemma used to shorten proofs. If a proposition is implied by (which is true, see vex 2724) and another antecedent, then it is implied by the other antecedent. (Contributed by Peter Mazsa, 23-Oct-2018.) |
Theorem | isset 2727* |
Two ways to say "
is a set": A class is a member of the
universal class (see df-v 2723) 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 4409. Note the when is not a set,
it is called a proper class. In some theorems, such as uniexg 4411, 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 2160 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 2728 | A version of isset that does not require x and A to be distinct. (Contributed by Andrew Salmon, 6-Jun-2011.) (Revised by Mario Carneiro, 10-Oct-2016.) |
Theorem | isseti 2729* | A way to say " is a set" (inference form). (Contributed by NM, 5-Aug-1993.) |
Theorem | issetri 2730* | A way to say " is a set" (inference form). (Contributed by NM, 5-Aug-1993.) |
Theorem | eqvisset 2731 | A class equal to a variable is a set. Note the absence of disjoint variable condition, contrary to isset 2727 and issetri 2730. (Contributed by BJ, 27-Apr-2019.) |
Theorem | elex 2732 | If a class is a member of another class, then it is a set. Theorem 6.12 of [Quine] p. 44. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | elexi 2733 | If a class is a member of another class, it is a set. (Contributed by NM, 11-Jun-1994.) |
Theorem | elexd 2734 | If a class is a member of another class, it is a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Theorem | elisset 2735* | An element of a class exists. (Contributed by NM, 1-May-1995.) |
Theorem | elex22 2736* | If two classes each contain another class, then both contain some set. (Contributed by Alan Sare, 24-Oct-2011.) |
Theorem | elex2 2737* | If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.) |
Theorem | ralv 2738 | A universal quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.) |
Theorem | rexv 2739 | An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.) |
Theorem | reuv 2740 | A unique existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 1-Nov-2010.) |
Theorem | rmov 2741 | An at-most-one quantifier restricted to the universe is unrestricted. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | rabab 2742 | 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 2743* | Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | rexcom4 2744* | Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | rexcom4a 2745* | Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.) |
Theorem | rexcom4b 2746* | Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.) |
Theorem | ceqsalt 2747* | Closed theorem version of ceqsalg 2749. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.) |
Theorem | ceqsralt 2748* | Restricted quantifier version of ceqsalt 2747. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.) |
Theorem | ceqsalg 2749* | A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 29-Oct-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | ceqsal 2750* | 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 2751* | 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 2752* | Restricted quantifier version of ceqsalv 2751. (Contributed by NM, 21-Jun-2013.) |
Theorem | gencl 2753* | Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.) |
Theorem | 2gencl 2754* | Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.) |
Theorem | 3gencl 2755* | Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.) |
Theorem | cgsexg 2756* | Implicit substitution inference for general classes. (Contributed by NM, 26-Aug-2007.) |
Theorem | cgsex2g 2757* | Implicit substitution inference for general classes. (Contributed by NM, 26-Jul-1995.) |
Theorem | cgsex4g 2758* | An implicit substitution inference for 4 general classes. (Contributed by NM, 5-Aug-1995.) |
Theorem | ceqsex 2759* | Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) (Revised by Mario Carneiro, 10-Oct-2016.) |
Theorem | ceqsexv 2760* | Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) |
Theorem | ceqsex2 2761* | Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.) |
Theorem | ceqsex2v 2762* | Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.) |
Theorem | ceqsex3v 2763* | Elimination of three existential quantifiers, using implicit substitution. (Contributed by NM, 16-Aug-2011.) |
Theorem | ceqsex4v 2764* | Elimination of four existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.) |
Theorem | ceqsex6v 2765* | Elimination of six existential quantifiers, using implicit substitution. (Contributed by NM, 21-Sep-2011.) |
Theorem | ceqsex8v 2766* | Elimination of eight existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.) |
Theorem | gencbvex 2767* | Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | gencbvex2 2768* | Restatement of gencbvex 2767 with weaker hypotheses. (Contributed by Jeff Hankins, 6-Dec-2006.) |
Theorem | gencbval 2769* | Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.) (Proof rewritten by Jim Kingdon, 20-Jun-2018.) |
Theorem | sbhypf 2770* | Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf . (Contributed by Raph Levien, 10-Apr-2004.) |
Theorem | vtoclgft 2771 | Closed theorem form of vtoclgf 2779. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 12-Oct-2016.) |
Theorem | vtocldf 2772 | Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.) |
Theorem | vtocld 2773* | Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.) |
Theorem | vtoclf 2774* | Implicit substitution of a class for a setvar variable. This is a generalization of chvar 1744. (Contributed by NM, 30-Aug-1993.) |
Theorem | vtocl 2775* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.) |
Theorem | vtocl2 2776* | Implicit substitution of classes for setvar variables. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | vtocl3 2777* | Implicit substitution of classes for setvar variables. (Contributed by NM, 3-Jun-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | vtoclb 2778* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 23-Dec-1993.) |
Theorem | vtoclgf 2779 | Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) (Proof shortened by Mario Carneiro, 10-Oct-2016.) |
Theorem | vtoclg1f 2780* | Version of vtoclgf 2779 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 1493 and ax-13 2137. (Contributed by BJ, 1-May-2019.) |
Theorem | vtoclg 2781* | Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) |
Theorem | vtoclbg 2782* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.) |
Theorem | vtocl2gf 2783 | Implicit substitution of a class for a setvar variable. (Contributed by NM, 25-Apr-1995.) |
Theorem | vtocl3gf 2784 | Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 10-Oct-2016.) |
Theorem | vtocl2g 2785* | Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) |
Theorem | vtoclgaf 2786* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.) |
Theorem | vtoclga 2787* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.) |
Theorem | vtocl2gaf 2788* | Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 10-Aug-2013.) |
Theorem | vtocl2ga 2789* | Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.) |
Theorem | vtocl3gaf 2790* | Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 11-Oct-2016.) |
Theorem | vtocl3ga 2791* | Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 20-Aug-1995.) |
Theorem | vtocleg 2792* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Jan-2004.) |
Theorem | vtoclegft 2793* | Implicit substitution of a class for a setvar variable. (Closed theorem version of vtoclef 2794.) (Contributed by NM, 7-Nov-2005.) (Revised by Mario Carneiro, 11-Oct-2016.) |
Theorem | vtoclef 2794* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 18-Aug-1993.) |
Theorem | vtocle 2795* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 9-Sep-1993.) |
Theorem | vtoclri 2796* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Nov-1994.) |
Theorem | spcimgft 2797 | A closed version of spcimgf 2801. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | spcgft 2798 | A closed version of spcgf 2803. (Contributed by Andrew Salmon, 6-Jun-2011.) (Revised by Mario Carneiro, 4-Jan-2017.) |
Theorem | spcimegft 2799 | A closed version of spcimegf 2802. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | spcegft 2800 | A closed version of spcegf 2804. (Contributed by Jim Kingdon, 22-Jun-2018.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |