Home | Metamath
Proof Explorer Theorem List (p. 37 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 | sseldi 3601 | Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.) |
Theorem | sseld 3602 | Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.) |
Theorem | sselda 3603 | Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.) |
Theorem | sseldd 3604 | Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.) |
Theorem | ssneld 3605 | If a class is not in another class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.) |
Theorem | ssneldd 3606 | If an element is not in a class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.) |
Theorem | ssriv 3607* | Inference rule based on subclass definition. (Contributed by NM, 21-Jun-1993.) |
Theorem | ssrd 3608 | Deduction rule based on subclass definition. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
Theorem | ssrdv 3609* | Deduction rule based on subclass definition. (Contributed by NM, 15-Nov-1995.) |
Theorem | sstr2 3610 | Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | sstr 3611 | Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.) |
Theorem | sstri 3612 | Subclass transitivity inference. (Contributed by NM, 5-May-2000.) |
Theorem | sstrd 3613 | Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.) |
Theorem | syl5ss 3614 | Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.) |
Theorem | syl6ss 3615 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | sylan9ss 3616 | A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | sylan9ssr 3617 | A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) |
Theorem | eqss 3618 | The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 21-May-1993.) |
Theorem | eqssi 3619 | Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.) |
Theorem | eqssd 3620 | Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.) |
Theorem | sssseq 3621 | If a class is a subclass of another class, the classes are equal iff the other class is a subclass of the first class. (Contributed by AV, 23-Dec-2020.) |
Theorem | eqrd 3622 | Deduce equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 21-Mar-2017.) (Proof shortened by BJ, 1-Dec-2021.) |
Theorem | eqrdOLD 3623 | Obsolete proof of eqrd 3622 as of 1-Dec-2021. (Contributed by Thierry Arnoux, 21-Mar-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ssid 3624 | Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | ssv 3625 | Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.) |
Theorem | sseq1 3626 | Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
Theorem | sseq2 3627 | Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.) |
Theorem | sseq12 3628 | Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999.) |
Theorem | sseq1i 3629 | An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.) |
Theorem | sseq2i 3630 | An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.) |
Theorem | sseq12i 3631 | An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
Theorem | sseq1d 3632 | An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.) |
Theorem | sseq2d 3633 | An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.) |
Theorem | sseq12d 3634 | An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.) |
Theorem | eqsstri 3635 | Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.) |
Theorem | eqsstr3i 3636 | Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.) |
Theorem | sseqtri 3637 | Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.) |
Theorem | sseqtr4i 3638 | Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.) |
Theorem | eqsstrd 3639 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
Theorem | eqsstr3d 3640 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
Theorem | sseqtrd 3641 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
Theorem | sseqtr4d 3642 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
Theorem | 3sstr3i 3643 | Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
Theorem | 3sstr4i 3644 | Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
Theorem | 3sstr3g 3645 | Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.) |
Theorem | 3sstr4g 3646 | Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
Theorem | 3sstr3d 3647 | Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.) |
Theorem | 3sstr4d 3648 | Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 30-Nov-1995.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
Theorem | syl5eqss 3649 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
Theorem | syl5eqssr 3650 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
Theorem | syl6sseq 3651 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
Theorem | syl6sseqr 3652 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
Theorem | syl5sseq 3653 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | syl5sseqr 3654 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | syl6eqss 3655 | A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Theorem | syl6eqssr 3656 | A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Theorem | eqimss 3657 | Equality implies the subclass relation. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
Theorem | eqimss2 3658 | Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.) |
Theorem | eqimssi 3659 | Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.) |
Theorem | eqimss2i 3660 | Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.) |
Theorem | nssne1 3661 | Two classes are different if they don't include the same class. (Contributed by NM, 23-Apr-2015.) |
Theorem | nssne2 3662 | Two classes are different if they are not subclasses of the same class. (Contributed by NM, 23-Apr-2015.) |
Theorem | nss 3663* | Negation of subclass relationship. Exercise 13 of [TakeutiZaring] p. 18. (Contributed by NM, 25-Feb-1996.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
Theorem | nelss 3664 | Demonstrate by witnesses that two classes lack a subclass relation. (Contributed by Stefan O'Rear, 5-Feb-2015.) |
Theorem | ssrexf 3665 | restricted existential quantification follows from a subclass relationship. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | ssralv 3666* | Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.) |
Theorem | ssrexv 3667* | Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.) |
Theorem | ralss 3668* | Restricted universal quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
Theorem | rexss 3669* | Restricted existential quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
Theorem | ss2ab 3670 | Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994.) |
Theorem | abss 3671* | Class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.) |
Theorem | ssab 3672* | Subclass of a class abstraction. (Contributed by NM, 16-Aug-2006.) |
Theorem | ssabral 3673* | The relation for a subclass of a class abstraction is equivalent to restricted quantification. (Contributed by NM, 6-Sep-2006.) |
Theorem | ss2abi 3674 | Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) |
Theorem | ss2abdv 3675* | Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) |
Theorem | abssdv 3676* | Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.) |
Theorem | abssi 3677* | Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.) |
Theorem | ss2rab 3678 | Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999.) |
Theorem | rabss 3679* | Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.) |
Theorem | ssrab 3680* | Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006.) |
Theorem | ssrabdv 3681* | Subclass of a restricted class abstraction (deduction rule). (Contributed by NM, 31-Aug-2006.) |
Theorem | rabssdv 3682* | Subclass of a restricted class abstraction (deduction rule). (Contributed by NM, 2-Feb-2015.) |
Theorem | ss2rabdv 3683* | Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.) |
Theorem | ss2rabi 3684 | Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.) |
Theorem | rabss2 3685* | Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | ssab2 3686* | Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995.) |
Theorem | ssrab2 3687* | Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.) |
Theorem | ssrab3 3688* | Subclass relation for a restricted class abstraction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | ssrabeq 3689* | If the restricting class of a restricted class abstraction is a subset of this restricted class abstraction, it is equal to this restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.) |
Theorem | rabssab 3690 | A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016.) |
Theorem | uniiunlem 3691* | A subset relationship useful for converting union to indexed union using dfiun2 4554 or dfiun2g 4552 and intersection to indexed intersection using dfiin2 4555. (Contributed by NM, 5-Oct-2006.) (Proof shortened by Mario Carneiro, 26-Sep-2015.) |
Theorem | dfpss2 3692 | Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) |
Theorem | dfpss3 3693 | Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | psseq1 3694 | Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.) |
Theorem | psseq2 3695 | Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.) |
Theorem | psseq1i 3696 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
Theorem | psseq2i 3697 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
Theorem | psseq12i 3698 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
Theorem | psseq1d 3699 | An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
Theorem | psseq2d 3700 | An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |