Home | Intuitionistic Logic Explorer Theorem List (p. 39 of 102) | < 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 | syl6eqbr 3801 | A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.) |
Theorem | syl6eqbrr 3802 | A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.) |
Theorem | syl6breq 3803 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
Theorem | syl6breqr 3804 | A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
Theorem | ssbrd 3805 | Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.) |
Theorem | ssbri 3806 | Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.) |
Theorem | nfbrd 3807 | Deduction version of bound-variable hypothesis builder nfbr 3808. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | nfbr 3808 | Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | brab1 3809* | Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.) |
Theorem | brun 3810 | The union of two binary relations. (Contributed by NM, 21-Dec-2008.) |
Theorem | brin 3811 | The intersection of two relations. (Contributed by FL, 7-Oct-2008.) |
Theorem | brdif 3812 | The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.) |
Theorem | sbcbrg 3813 | 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 3814* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
Theorem | sbcbr1g 3815* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
Theorem | sbcbr2g 3816* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
Syntax | copab 3817 | Extend class notation to include ordered-pair class abstraction (class builder). |
Syntax | cmpt 3818 | Extend the definition of a class to include maps-to notation for defining a function via a rule. |
Definition | df-opab 3819* | 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 3820* | 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 3821* | 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 3822 | 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 3823* | Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (Contributed by NM, 15-May-1995.) |
Theorem | opabbii 3824 | Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
Theorem | nfopab 3825* | 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 3826 | 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 3827 | 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 3828* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.) |
Theorem | cbvopabv 3829* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.) |
Theorem | cbvopab1 3830* | 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 3831* | Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.) |
Theorem | cbvopab1s 3832* | Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.) |
Theorem | cbvopab1v 3833* | 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 3834* | Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.) |
Theorem | csbopabg 3835* | Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
Theorem | unopab 3836 | Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) |
Theorem | mpteq12f 3837 | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq12dva 3838* | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Theorem | mpteq12dv 3839* | An equality inference for the maps to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq12 3840* | An equality theorem for the maps to notation. (Contributed by NM, 16-Dec-2013.) |
Theorem | mpteq1 3841* | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq1d 3842* | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 11-Jun-2016.) |
Theorem | mpteq2ia 3843 | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq2i 3844 | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq12i 3845 | An equality inference for the maps to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq2da 3846 | 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 3847* | Slightly more general equality inference for the maps to notation. (Contributed by Scott Fenton, 25-Apr-2012.) |
Theorem | mpteq2dv 3848* | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 23-Aug-2014.) |
Theorem | nfmpt 3849* | Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |
Theorem | nfmpt1 3850 | Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.) |
Theorem | cbvmpt 3851* | 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 3852* | Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) |
Theorem | mptv 3853* | Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.) |
Syntax | wtr 3854 | Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35. |
Definition | df-tr 3855 | Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3856 (which is suggestive of the word "transitive"), dftr3 3858, dftr4 3859, and dftr5 3857. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.) |
Theorem | dftr2 3856* | An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.) |
Theorem | dftr5 3857* | An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.) |
Theorem | dftr3 3858* | An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.) |
Theorem | dftr4 3859 | An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.) |
Theorem | treq 3860 | Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.) |
Theorem | trel 3861 | 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 3862 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) |
Theorem | trss 3863 | An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.) |
Theorem | trin 3864 | The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.) |
Theorem | tr0 3865 | The empty set is transitive. (Contributed by NM, 16-Sep-1993.) |
Theorem | trv 3866 | The universe is transitive. (Contributed by NM, 14-Sep-2003.) |
Theorem | triun 3867* | The indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.) |
Theorem | truni 3868* | 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 3869* | 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 3870* | If is transitive and inhabited, then is a subset of . (Contributed by Jim Kingdon, 22-Aug-2018.) |
Theorem | trint0m 3871* | Any inhabited transitive class includes its intersection. Similar to Exercise 2 in [TakeutiZaring] p. 44. (Contributed by Jim Kingdon, 22-Aug-2018.) |
Axiom | ax-coll 3872* | Axiom of Collection. Axiom 7 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). It is similar to bnd 3925 but uses a freeness hypothesis in place of one of the distinct variable constraints. (Contributed by Jim Kingdon, 23-Aug-2018.) |
Theorem | repizf 3873* | 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 3872. It is identical to zfrep6 3874 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 3874* | A version of the Axiom of Replacement. Normally would have free variables and . Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 3875 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 3875* |
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 2763. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. (Contributed by NM, 11-Sep-2006.) |
Theorem | axsep2 3876* | A less restrictive version of the Separation Scheme ax-sep 3875, 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 3875 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
Theorem | zfauscl 3877* | Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 3875, we invoke the Axiom of Extensionality (indirectly via vtocl 2608), which is needed for the justification of class variable notation. (Contributed by NM, 5-Aug-1993.) |
Theorem | bm1.3ii 3878* | Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 3875. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.) |
Theorem | a9evsep 3879* | Derive a weakened version of ax-i9 1423, where and must be distinct, from Separation ax-sep 3875 and Extensionality ax-ext 2022. The theorem also holds (ax9vsep 3880), but in intuitionistic logic is stronger. (Contributed by Jim Kingdon, 25-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax9vsep 3880* | Derive a weakened version of ax-9 1424, where and must be distinct, from Separation ax-sep 3875 and Extensionality ax-ext 2022. In intuitionistic logic a9evsep 3879 is stronger and also holds. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | zfnuleu 3881* | Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2025 to strengthen the hypothesis in the form of axnul 3882). (Contributed by NM, 22-Dec-2007.) |
Theorem | axnul 3882* |
The Null Set Axiom of ZF set theory: there exists a set with no
elements. Axiom of Empty Set of [Enderton] p. 18. In some textbooks,
this is presented as a separate axiom; here we show it can be derived
from Separation ax-sep 3875. This version of the Null Set Axiom tells us
that at least one empty set exists, but does not tell us that it is
unique - we need the Axiom of Extensionality to do that (see
zfnuleu 3881).
This theorem should not be referenced by any proof. Instead, use ax-nul 3883 below so that the uses of the Null Set Axiom can be more easily identified. (Contributed by Jeff Hoffman, 3-Feb-2008.) (Revised by NM, 4-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
Axiom | ax-nul 3883* | The Null Set Axiom of IZF set theory. It was derived as axnul 3882 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. Axiom 4 of [Crosilla] p. "Axioms of CZF and IZF". (Contributed by NM, 7-Aug-2003.) |
Theorem | 0ex 3884 | The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 3883. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | csbexga 3885 | The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Theorem | csbexa 3886 | The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | nalset 3887* | No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.) |
Theorem | vprc 3888 | The universal class is not a member of itself (and thus is not a set). Proposition 5.21 of [TakeutiZaring] p. 21; our proof, however, does not depend on the Axiom of Regularity. (Contributed by NM, 23-Aug-1993.) |
Theorem | nvel 3889 | The universal class doesn't belong to any class. (Contributed by FL, 31-Dec-2006.) |
Theorem | vnex 3890 | The universal class does not exist. (Contributed by NM, 4-Jul-2005.) |
Theorem | inex1 3891 | Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.) |
Theorem | inex2 3892 | Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.) |
Theorem | inex1g 3893 | Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.) |
Theorem | ssex 3894 | The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 3875 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.) |
Theorem | ssexi 3895 | The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.) |
Theorem | ssexg 3896 | The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) |
Theorem | ssexd 3897 | A subclass of a set is a set. Deduction form of ssexg 3896. (Contributed by David Moews, 1-May-2017.) |
Theorem | difexg 3898 | Existence of a difference. (Contributed by NM, 26-May-1998.) |
Theorem | zfausab 3899* | Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.) |
Theorem | rabexg 3900* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |