Home | Metamath
Proof Explorer Theorem List (p. 379 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 | arearect 37801 | The area of a rectangle whose sides are parallel to the coordinate axes in is its width multiplied by its height. (Contributed by Jon Pennant, 19-Mar-2019.) |
area | ||
Theorem | areaquad 37802* | The area of a quadrilateral with two sides which are parallel to the y-axis in is its width multiplied by the average height of its higher edge minus the average height of its lower edge. Co-author TA. (Contributed by Jon Pennant, 31-May-2019.) |
area | ||
Theorem | ifpan123g 37803 | Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
if- if- | ||
Theorem | ifpan23 37804 | Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.) |
if- if- if- | ||
Theorem | ifpdfor2 37805 | Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
if- | ||
Theorem | ifporcor 37806 | Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.) |
if- if- | ||
Theorem | ifpdfan2 37807 | Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
if- | ||
Theorem | ifpancor 37808 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
if- if- | ||
Theorem | ifpdfor 37809 | Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.) |
if- | ||
Theorem | ifpdfan 37810 | Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.) |
if- | ||
Theorem | ifpbi2 37811 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
if- if- | ||
Theorem | ifpbi3 37812 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
if- if- | ||
Theorem | ifpim1 37813 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
if- | ||
Theorem | ifpnot 37814 | Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
if- | ||
Theorem | ifpid2 37815 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
if- | ||
Theorem | ifpim2 37816 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
if- | ||
Theorem | ifpbi23 37817 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
if- if- | ||
Theorem | ifpdfbi 37818 | Define biimplication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
if- | ||
Theorem | ifpbiidcor 37819 | Restatement of biid 251. (Contributed by RP, 25-Apr-2020.) |
if- | ||
Theorem | ifpbicor 37820 | Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.) |
if- if- | ||
Theorem | ifpxorcor 37821 | Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.) |
if- if- | ||
Theorem | ifpbi1 37822 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
if- if- | ||
Theorem | ifpnot23 37823 | Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.) |
if- if- | ||
Theorem | ifpnotnotb 37824 | Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
if- if- | ||
Theorem | ifpnorcor 37825 | Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.) |
if- if- | ||
Theorem | ifpnancor 37826 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
if- if- | ||
Theorem | ifpnot23b 37827 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
if- if- | ||
Theorem | ifpbiidcor2 37828 | Restatement of biid 251. (Contributed by RP, 25-Apr-2020.) |
if- | ||
Theorem | ifpnot23c 37829 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
if- if- | ||
Theorem | ifpnot23d 37830 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
if- if- | ||
Theorem | ifpdfnan 37831 | Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
if- | ||
Theorem | ifpdfxor 37832 | Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
if- | ||
Theorem | ifpbi12 37833 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
if- if- | ||
Theorem | ifpbi13 37834 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
if- if- | ||
Theorem | ifpbi123 37835 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
if- if- | ||
Theorem | ifpidg 37836 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
if- | ||
Theorem | ifpid3g 37837 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
if- | ||
Theorem | ifpid2g 37838 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
if- | ||
Theorem | ifpid1g 37839 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
if- | ||
Theorem | ifpim23g 37840 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
if- | ||
Theorem | ifpim3 37841 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
if- | ||
Theorem | ifpnim1 37842 | Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
if- | ||
Theorem | ifpim4 37843 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
if- | ||
Theorem | ifpnim2 37844 | Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
if- | ||
Theorem | ifpim123g 37845 | Implication of conditional logical operators. The right hand side is basically conjunctive normal form which is useful in proofs. (Contributed by RP, 16-Apr-2020.) |
if- if- | ||
Theorem | ifpim1g 37846 | Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
if- if- | ||
Theorem | ifp1bi 37847 | Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020.) |
if- if- | ||
Theorem | ifpbi1b 37848 | When the first variable is irrelevant, it can be replaced. (Contributed by RP, 25-Apr-2020.) |
if- if- | ||
Theorem | ifpimimb 37849 | Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
if- if- if- | ||
Theorem | ifpororb 37850 | Factor conditional logic operator over disjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
if- if- if- | ||
Theorem | ifpananb 37851 | Factor conditional logic operator over conjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
if- if- if- | ||
Theorem | ifpnannanb 37852 | Factor conditional logic operator over nand in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
if- if- if- | ||
Theorem | ifpor123g 37853 | Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
if- if- | ||
Theorem | ifpimim 37854 | Consequnce of implication. (Contributed by RP, 17-Apr-2020.) |
if- if- if- | ||
Theorem | ifpbibib 37855 | Factor conditional logic operator over biimplication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
if- if- if- | ||
Theorem | ifpxorxorb 37856 | Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
if- if- if- | ||
Theorem | rp-fakeimass 37857 | A special case where implication appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.) |
Theorem | rp-fakeanorass 37858 | A special case where a mixture of and and or appears to conform to a mixed associative law. (Contributed by Richard Penner, 26-Feb-2020.) |
Theorem | rp-fakeoranass 37859 | A special case where a mixture of or and and appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.) |
Theorem | rp-fakenanass 37860 | A special case where nand appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.) |
Theorem | rp-fakeinunass 37861 | A special case where a mixture of intersection and union appears to conform to a mixed associative law. (Contributed by Richard Penner, 26-Feb-2020.) |
Theorem | rp-fakeuninass 37862 | A special case where a mixture of union and intersection appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.) |
Membership in the class of finite sets can be expressed in many ways. | ||
Theorem | rp-isfinite5 37863* | A set is said to be finite if it can be put in one-to-one correspondence with all the natural numbers between 1 and some . (Contributed by Richard Penner, 3-Mar-2020.) |
Theorem | rp-isfinite6 37864* | A set is said to be finite if it is either empty or it can be put in one-to-one correspondence with all the natural numbers between 1 and some . (Contributed by Richard Penner, 10-Mar-2020.) |
Theorem | pwelg 37865* | The powerclass is an element of a class closed under union and powerclass operations iff the element is a member of that class. (Contributed by RP, 21-Mar-2020.) |
Theorem | pwinfig 37866* | The powerclass of an infinite set is an infinite set, and vice-versa. Here is a class which is closed under both the union and the powerclass operations and which may have infinite sets as members. (Contributed by RP, 21-Mar-2020.) |
Theorem | pwinfi2 37867 | The powerclass of an infinite set is an infinite set, and vice-versa. Here is a weak universe. (Contributed by RP, 21-Mar-2020.) |
WUni | ||
Theorem | pwinfi3 37868 | The powerclass of an infinite set is an infinite set, and vice-versa. Here is a transitive Tarski universe. (Contributed by RP, 21-Mar-2020.) |
Theorem | pwinfi 37869 | The powerclass of an infinite set is an infinite set, and vice-versa. (Contributed by RP, 21-Mar-2020.) |
While there is not yet a definition, the finite intersection property of a class is introduced by fiint 8237 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 5754, ordelinel 5825), chains of sets ordered by the proper subset relation (sorpssin 6945), various sets in the field of topology (inopn 20704, incld 20847, innei 20929, ... ) and "universal" classes like weak universes (wunin 9535, tskin 9581) and the class of all sets (inex1g 4801). | ||
Theorem | fipjust 37870* | A definition of the finite intersection property of a class based on closure under pairwise intersection of its elements is independent of the dummy variables. (Contributed by Richard Penner, 1-Jan-2020.) |
Theorem | cllem0 37871* | The class of all sets with property is closed under the binary operation on sets defined in . (Contributed by Richard Penner, 3-Jan-2020.) |
Theorem | superficl 37872* | The class of all supersets of a class has the finite intersection property. (Contributed by Richard Penner, 1-Jan-2020.) (Proof shortened by Richard Penner, 3-Jan-2020.) |
Theorem | superuncl 37873* | The class of all supersets of a class is closed under binary union. (Contributed by Richard Penner, 3-Jan-2020.) |
Theorem | ssficl 37874* | The class of all subsets of a class has the finite intersection property. (Contributed by Richard Penner, 1-Jan-2020.) (Proof shortened by Richard Penner, 3-Jan-2020.) |
Theorem | ssuncl 37875* | The class of all subsets of a class is closed under binary union. (Contributed by Richard Penner, 3-Jan-2020.) |
Theorem | ssdifcl 37876* | The class of all subsets of a class is closed under class difference. (Contributed by Richard Penner, 3-Jan-2020.) |
Theorem | sssymdifcl 37877* | The class of all subsets of a class is closed under symmetric difference. (Contributed by Richard Penner, 3-Jan-2020.) |
Theorem | fiinfi 37878* | If two classes have the finite intersection property, then so does their intersection. (Contributed by Richard Penner, 1-Jan-2020.) |
Theorem | rababg 37879 | Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020.) |
Theorem | elintabg 37880* | Two ways of saying a set is an element of the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
Theorem | elinintab 37881* | Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
Theorem | elmapintrab 37882* | Two ways to say a set is an element of the intersection of a class of images. (Contributed by RP, 16-Aug-2020.) |
Theorem | elinintrab 37883* | Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 14-Aug-2020.) |
Theorem | inintabss 37884* | Upper bound on intersection of class and the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
Theorem | inintabd 37885* | Value of the intersection of class with the intersection of a non-empty class. (Contributed by RP, 13-Aug-2020.) |
Theorem | xpinintabd 37886* | Value of the intersection of cross-product with the intersection of a non-empty class. (Contributed by RP, 12-Aug-2020.) |
Theorem | relintabex 37887 | If the intersection of a class is a relation, then the class is non-empty. (Contributed by RP, 12-Aug-2020.) |
Theorem | elcnvcnvintab 37888* | Two ways of saying a set is an element of the converse of the converse of the intersection of a class. (Contributed by RP, 20-Aug-2020.) |
Theorem | relintab 37889* | Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020.) |
Theorem | nonrel 37890 | A non-relation is equal to the base class with all ordered pairs removed. (Contributed by RP, 25-Oct-2020.) |
Theorem | elnonrel 37891 | Only an ordered pair where not both entries are sets could be an element of the non-relation part of class. (Contributed by RP, 25-Oct-2020.) |
Theorem | cnvssb 37892 | Subclass theorem for converse. (Contributed by RP, 22-Oct-2020.) |
Theorem | relnonrel 37893 | The non-relation part of a relation is empty. (Contributed by RP, 22-Oct-2020.) |
Theorem | cnvnonrel 37894 | The converse of the non-relation part of a class is empty. (Contributed by RP, 18-Oct-2020.) |
Theorem | brnonrel 37895 | A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020.) |
Theorem | dmnonrel 37896 | The domain of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
Theorem | rnnonrel 37897 | The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
Theorem | resnonrel 37898 | A restriction of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
Theorem | imanonrel 37899 | An image under the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
Theorem | cononrel1 37900 | Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |