Home | Intuitionistic Logic Explorer Theorem List (p. 39 of 108) | < 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 | breqan12rd 3801 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
Theorem | nbrne1 3802 | Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.) |
Theorem | nbrne2 3803 | Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.) |
Theorem | eqbrtri 3804 | Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.) |
Theorem | eqbrtrd 3805 | Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.) |
Theorem | eqbrtrri 3806 | Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.) |
Theorem | eqbrtrrd 3807 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
Theorem | breqtri 3808 | Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.) |
Theorem | breqtrd 3809 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
Theorem | breqtrri 3810 | Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.) |
Theorem | breqtrrd 3811 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
Theorem | 3brtr3i 3812 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.) |
Theorem | 3brtr4i 3813 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.) |
Theorem | 3brtr3d 3814 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.) |
Theorem | 3brtr4d 3815 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.) |
Theorem | 3brtr3g 3816 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.) |
Theorem | 3brtr4g 3817 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.) |
Theorem | syl5eqbr 3818 | B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
Theorem | syl5eqbrr 3819 | B chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.) |
Theorem | syl5breq 3820 | B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
Theorem | syl5breqr 3821 | B chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
Theorem | syl6eqbr 3822 | A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.) |
Theorem | syl6eqbrr 3823 | A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.) |
Theorem | syl6breq 3824 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
Theorem | syl6breqr 3825 | A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
Theorem | ssbrd 3826 | Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.) |
Theorem | ssbri 3827 | Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.) |
Theorem | nfbrd 3828 | Deduction version of bound-variable hypothesis builder nfbr 3829. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | nfbr 3829 | Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | brab1 3830* | Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.) |
Theorem | brun 3831 | The union of two binary relations. (Contributed by NM, 21-Dec-2008.) |
Theorem | brin 3832 | The intersection of two relations. (Contributed by FL, 7-Oct-2008.) |
Theorem | brdif 3833 | The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.) |
Theorem | sbcbrg 3834 | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | sbcbr12g 3835* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
Theorem | sbcbr1g 3836* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
Theorem | sbcbr2g 3837* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
Syntax | copab 3838 | Extend class notation to include ordered-pair class abstraction (class builder). |
Syntax | cmpt 3839 | Extend the definition of a class to include maps-to notation for defining a function via a rule. |
Definition | df-opab 3840* | Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually and are distinct, although the definition doesn't strictly require it. The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by NM, 4-Jul-1994.) |
Definition | df-mpt 3841* | Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from (in ) to ." The class expression is the value of the function at and normally contains the variable . Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.) |
Theorem | opabss 3842* | The collection of ordered pairs in a class is a subclass of it. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | opabbid 3843 | Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | opabbidv 3844* | Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (Contributed by NM, 15-May-1995.) |
Theorem | opabbii 3845 | Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
Theorem | nfopab 3846* | Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.) |
Theorem | nfopab1 3847 | The first abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | nfopab2 3848 | The second abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | cbvopab 3849* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.) |
Theorem | cbvopabv 3850* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.) |
Theorem | cbvopab1 3851* | Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | cbvopab2 3852* | Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.) |
Theorem | cbvopab1s 3853* | Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.) |
Theorem | cbvopab1v 3854* | Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) |
Theorem | cbvopab2v 3855* | Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.) |
Theorem | csbopabg 3856* | Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
Theorem | unopab 3857 | Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) |
Theorem | mpteq12f 3858 | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq12dva 3859* | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Theorem | mpteq12dv 3860* | An equality inference for the maps to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq12 3861* | An equality theorem for the maps to notation. (Contributed by NM, 16-Dec-2013.) |
Theorem | mpteq1 3862* | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq1d 3863* | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 11-Jun-2016.) |
Theorem | mpteq2ia 3864 | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq2i 3865 | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq12i 3866 | An equality inference for the maps to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq2da 3867 | Slightly more general equality inference for the maps to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq2dva 3868* | Slightly more general equality inference for the maps to notation. (Contributed by Scott Fenton, 25-Apr-2012.) |
Theorem | mpteq2dv 3869* | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 23-Aug-2014.) |
Theorem | nfmpt 3870* | Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |
Theorem | nfmpt1 3871 | Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.) |
Theorem | cbvmpt 3872* | Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.) |
Theorem | cbvmptv 3873* | Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) |
Theorem | mptv 3874* | Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.) |
Syntax | wtr 3875 | Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35. |
Definition | df-tr 3876 | Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3877 (which is suggestive of the word "transitive"), dftr3 3879, dftr4 3880, and dftr5 3878. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.) |
Theorem | dftr2 3877* | An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.) |
Theorem | dftr5 3878* | An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.) |
Theorem | dftr3 3879* | An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.) |
Theorem | dftr4 3880 | An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.) |
Theorem | treq 3881 | Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.) |
Theorem | trel 3882 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | trel3 3883 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) |
Theorem | trss 3884 | An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.) |
Theorem | trin 3885 | The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.) |
Theorem | tr0 3886 | The empty set is transitive. (Contributed by NM, 16-Sep-1993.) |
Theorem | trv 3887 | The universe is transitive. (Contributed by NM, 14-Sep-2003.) |
Theorem | triun 3888* | The indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.) |
Theorem | truni 3889* | The union of a class of transitive sets is transitive. Exercise 5(a) of [Enderton] p. 73. (Contributed by Scott Fenton, 21-Feb-2011.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |
Theorem | trint 3890* | The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. (Contributed by Scott Fenton, 25-Feb-2011.) |
Theorem | trintssm 3891* | Any inhabited transitive class includes its intersection. Similar to Exercise 3 in [TakeutiZaring] p. 44 (which mistakenly does not include the inhabitedness hypothesis). (Contributed by Jim Kingdon, 22-Aug-2018.) |
Theorem | trintssmOLD 3892* | Obsolete version of trintssm 3891 as of 30-Oct-2021. (Contributed by Jim Kingdon, 22-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
Axiom | ax-coll 3893* | Axiom of Collection. Axiom 7 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). It is similar to bnd 3946 but uses a freeness hypothesis in place of one of the distinct variable constraints. (Contributed by Jim Kingdon, 23-Aug-2018.) |
Theorem | repizf 3894* | Axiom of Replacement. Axiom 7' of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). In our context this is not an axiom, but a theorem proved from ax-coll 3893. It is identical to zfrep6 3895 except for the choice of a freeness hypothesis rather than a distinct variable constraint between and . (Contributed by Jim Kingdon, 23-Aug-2018.) |
Theorem | zfrep6 3895* | A version of the Axiom of Replacement. Normally would have free variables and . Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 3896 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version. (Contributed by NM, 10-Oct-2003.) |
Axiom | ax-sep 3896* |
The Axiom of Separation of IZF set theory. Axiom 6 of [Crosilla], p.
"Axioms of CZF and IZF" (with unnecessary quantifier removed,
and with a
condition replaced by a distinct
variable constraint between
and ).
The Separation Scheme is a weak form of Frege's Axiom of Comprehension, conditioning it (with ) so that it asserts the existence of a collection only if it is smaller than some other collection that already exists. This prevents Russell's paradox ru 2814. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. (Contributed by NM, 11-Sep-2006.) |
Theorem | axsep2 3897* | A less restrictive version of the Separation Scheme ax-sep 3896, where variables and can both appear free in the wff , which can therefore be thought of as . This version was derived from the more restrictive ax-sep 3896 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
Theorem | zfauscl 3898* | Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 3896, we invoke the Axiom of Extensionality (indirectly via vtocl 2653), which is needed for the justification of class variable notation. (Contributed by NM, 5-Aug-1993.) |
Theorem | bm1.3ii 3899* | Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 3896. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.) |
Theorem | a9evsep 3900* | Derive a weakened version of ax-i9 1463, where and must be distinct, from Separation ax-sep 3896 and Extensionality ax-ext 2063. The theorem also holds (ax9vsep 3901), but in intuitionistic logic is stronger. (Contributed by Jim Kingdon, 25-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |