Home | Intuitionistic Logic Explorer Theorem List (p. 41 of 139) | < 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 | breqtri 4001 | Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.) |
Theorem | breqtrd 4002 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
Theorem | breqtrri 4003 | Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.) |
Theorem | breqtrrd 4004 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
Theorem | 3brtr3i 4005 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.) |
Theorem | 3brtr4i 4006 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.) |
Theorem | 3brtr3d 4007 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.) |
Theorem | 3brtr4d 4008 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.) |
Theorem | 3brtr3g 4009 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.) |
Theorem | 3brtr4g 4010 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.) |
Theorem | eqbrtrid 4011 | B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
Theorem | eqbrtrrid 4012 | B chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.) |
Theorem | breqtrid 4013 | B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
Theorem | breqtrrid 4014 | B chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
Theorem | eqbrtrdi 4015 | A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.) |
Theorem | eqbrtrrdi 4016 | A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.) |
Theorem | breqtrdi 4017 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
Theorem | breqtrrdi 4018 | A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
Theorem | ssbrd 4019 | Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.) |
Theorem | ssbri 4020 | Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.) |
Theorem | nfbrd 4021 | Deduction version of bound-variable hypothesis builder nfbr 4022. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | nfbr 4022 | Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | brab1 4023* | Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.) |
Theorem | br0 4024 | The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.) |
Theorem | brne0 4025 | If two sets are in a binary relation, the relation cannot be empty. In fact, the relation is also inhabited, as seen at brm 4026. (Contributed by Alexander van der Vekens, 7-Jul-2018.) |
Theorem | brm 4026* | If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.) |
Theorem | brun 4027 | The union of two binary relations. (Contributed by NM, 21-Dec-2008.) |
Theorem | brin 4028 | The intersection of two relations. (Contributed by FL, 7-Oct-2008.) |
Theorem | brdif 4029 | The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.) |
Theorem | sbcbrg 4030 | 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 4031* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
Theorem | sbcbr1g 4032* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
Theorem | sbcbr2g 4033* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
Theorem | brralrspcev 4034* | Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.) |
Theorem | brimralrspcev 4035* | Restricted existential specialization with a restricted universal quantifier over an implication with a relation in the antecedent, closed form. (Contributed by AV, 20-Aug-2022.) |
Syntax | copab 4036 | Extend class notation to include ordered-pair class abstraction (class builder). |
Syntax | cmpt 4037 | Extend the definition of a class to include maps-to notation for defining a function via a rule. |
Definition | df-opab 4038* | 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 4039* | 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 4040* | 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 4041 | Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | opabbidv 4042* | Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.) |
Theorem | opabbii 4043 | Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
Theorem | nfopab 4044* | Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | nfopab1 4045 | 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 4046 | 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 4047* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.) |
Theorem | cbvopabv 4048* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.) |
Theorem | cbvopab1 4049* | 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 4050* | Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.) |
Theorem | cbvopab1s 4051* | Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.) |
Theorem | cbvopab1v 4052* | 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 4053* | Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.) |
Theorem | csbopabg 4054* | Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
Theorem | unopab 4055 | Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) |
Theorem | mpteq12f 4056 | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq12dva 4057* | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Theorem | mpteq12dv 4058* | An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq12 4059* | An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.) |
Theorem | mpteq1 4060* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq1d 4061* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.) |
Theorem | mpteq2ia 4062 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq2i 4063 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq12i 4064 | An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq2da 4065 | 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 4066* | Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) |
Theorem | mpteq2dv 4067* | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.) |
Theorem | nfmpt 4068* | Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |
Theorem | nfmpt1 4069 | Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.) |
Theorem | cbvmptf 4070* | 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 Thierry Arnoux, 9-Mar-2017.) |
Theorem | cbvmpt 4071* | 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 4072* | Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) |
Theorem | mptv 4073* | Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.) |
Syntax | wtr 4074 | Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35. |
Definition | df-tr 4075 | Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4076 (which is suggestive of the word "transitive"), dftr3 4078, dftr4 4079, and dftr5 4077. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.) |
Theorem | dftr2 4076* | An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.) |
Theorem | dftr5 4077* | An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.) |
Theorem | dftr3 4078* | An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.) |
Theorem | dftr4 4079 | An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.) |
Theorem | treq 4080 | Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.) |
Theorem | trel 4081 | 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 4082 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) |
Theorem | trss 4083 | An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.) |
Theorem | trin 4084 | The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.) |
Theorem | tr0 4085 | The empty set is transitive. (Contributed by NM, 16-Sep-1993.) |
Theorem | trv 4086 | The universe is transitive. (Contributed by NM, 14-Sep-2003.) |
Theorem | triun 4087* | The indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.) |
Theorem | truni 4088* | 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 4089* | 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 4090* | 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.) |
Axiom | ax-coll 4091* | Axiom of Collection. Axiom 7 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). It is similar to bnd 4145 but uses a freeness hypothesis in place of one of the distinct variable conditions. (Contributed by Jim Kingdon, 23-Aug-2018.) |
Theorem | repizf 4092* | 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 4091. It is identical to zfrep6 4093 except for the choice of a freeness hypothesis rather than a disjoint variable condition between and . (Contributed by Jim Kingdon, 23-Aug-2018.) |
Theorem | zfrep6 4093* | A version of the Axiom of Replacement. Normally would have free variables and . Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 4094 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 4094* |
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 disjoint
variable condition 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 2945. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. (Contributed by NM, 11-Sep-2006.) |
Theorem | axsep2 4095* | A less restrictive version of the Separation Scheme ax-sep 4094, 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 4094 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
Theorem | zfauscl 4096* | Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 4094, we invoke the Axiom of Extensionality (indirectly via vtocl 2775), which is needed for the justification of class variable notation. (Contributed by NM, 5-Aug-1993.) |
Theorem | bm1.3ii 4097* | Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4094. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.) |
Theorem | a9evsep 4098* | Derive a weakened version of ax-i9 1517, where and must be distinct, from Separation ax-sep 4094 and Extensionality ax-ext 2146. The theorem also holds (ax9vsep 4099), but in intuitionistic logic is stronger. (Contributed by Jim Kingdon, 25-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax9vsep 4099* | Derive a weakened version of ax-9 1518, where and must be distinct, from Separation ax-sep 4094 and Extensionality ax-ext 2146. In intuitionistic logic a9evsep 4098 is stronger and also holds. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | zfnuleu 4100* | Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2149 to strengthen the hypothesis in the form of axnul 4101). (Contributed by NM, 22-Dec-2007.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |