Home | Metamath
Proof Explorer Theorem List (p. 341 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 | eqeltr 34001 | Substitution of equal classes into elementhood relation. (Contributed by Peter Mazsa, 22-Jul-2017.) |
Theorem | eqelb 34002 | Substitution of equal classes into elementhood relation. (Contributed by Peter Mazsa, 17-Jul-2019.) |
Theorem | eqeqan1d 34003 | Implication of introducing a new equality. (Contributed by Peter Mazsa, 17-Apr-2019.) |
Theorem | eqeqan2d 34004 | Implication of introducing a new equality. (Contributed by Peter Mazsa, 17-Apr-2019.) |
Theorem | ineqcom 34005 | Two ways of saying that two classes are disjoint (when : ). (Contributed by Peter Mazsa, 22-Mar-2017.) |
Theorem | ineqcomi 34006 | Disjointness inference (when ), inference form of ineqcom 34005. (Contributed by Peter Mazsa, 26-Mar-2017.) |
Theorem | inres2 34007 | Two ways of expressing the restriction of an intersection. (Contributed by Peter Mazsa, 5-Jun-2021.) |
Theorem | ssbr 34008 | Subclass theorem for binary relation, in a more searchable form: . (Contributed by Peter Mazsa, 11-Nov-2019.) |
Theorem | coideq 34009 | Equality theorem for composition of two classes. (Contributed by Peter Mazsa, 23-Sep-2021.) |
Theorem | ralanid 34010 | Cancellation law for restriction. (Contributed by Peter Mazsa, 30-Dec-2018.) |
Theorem | nexmo 34011 | If there is no case where wff is true, it is true for at most one case. (Contributed by Peter Mazsa, 27-Sep-2021.) |
Theorem | 3albii 34012 | Inference adding three universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 10-Aug-2018.) |
Theorem | 3ralbii 34013 | Inference adding three restricted universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 25-Jul-2019.) |
Theorem | rabbii 34014 | Equivalent wff's correspond to equal restricted class abstractions. (Contributed by Peter Mazsa, 1-Nov-2019.) |
Theorem | rabbieq 34015 | Equivalent wff's correspond to restricted class abstractions which are equal with the same class. (Contributed by Peter Mazsa, 8-Jul-2019.) |
Theorem | rabimbieq 34016 | Restricted equivalent wff's correspond to restricted class abstractions which are equal with the same class. (Contributed by Peter Mazsa, 22-Jul-2021.) |
Theorem | abeqin 34017* | Intersection with class abstraction. (Contributed by Peter Mazsa, 21-Jul-2021.) |
Theorem | abeqinbi 34018* | Intersection with class abstraction and equivalent wff's. (Contributed by Peter Mazsa, 21-Jul-2021.) |
Theorem | rabeqel 34019* | Class element of a restricted class abstraction. (Contributed by Peter Mazsa, 24-Jul-2021.) |
Theorem | eqrelf 34020* | The equality connective between relations. (Contributed by Peter Mazsa, 25-Jun-2019.) |
Theorem | releleccnv 34021 | Elementhood in a converse -coset when is a relation. (Contributed by Peter Mazsa, 9-Dec-2018.) |
Theorem | releccnveq 34022* | Equality of converse -coset and converse -coset when and are relations. (Contributed by Peter Mazsa, 27-Jul-2019.) |
Theorem | opelvvdif 34023 | Negated elementhood of ordered pair. (Contributed by Peter Mazsa, 14-Jan-2019.) |
Theorem | vvdifopab 34024* | Ordered-pair class abstraction defined by a negation. (Contributed by Peter Mazsa, 25-Jun-2019.) |
Theorem | brvdif 34025 | Binary relation with universal complement is the negation of the relation. (Contributed by Peter Mazsa, 1-Jul-2018.) |
Theorem | brvdif2 34026 | Binary relation with universal complement. (Contributed by Peter Mazsa, 14-Jul-2018.) |
Theorem | brvvdif 34027 | Binary relation with the complement under the universal class of ordered pairs. (Contributed by Peter Mazsa, 9-Nov-2018.) |
Theorem | brvbrvvdif 34028 | Binary relation with the complement under the universal class of ordered pairs is the same as with universal complement. (Contributed by Peter Mazsa, 28-Nov-2018.) |
Theorem | brcnvep 34029 | The converse of the binary epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018.) |
Theorem | elecALTV 34030 | Elementhood in the -coset of . Theorem 72 of [Suppes] p. 82. (I think we should replace elecg 7785 with this original form of Suppes. Peter Mazsa) (Contributed by Mario Carneiro, 9-Jul-2014.) |
Theorem | opelresALTV 34031 | Ordered pair elementhood in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 13-Nov-1995.) |
Theorem | brresALTV 34032 | Binary relation on a restriction. (Contributed by Mario Carneiro, 4-Nov-2015.) |
Theorem | brcnvepres 34033 | Restricted converse epsilon binary relation. (Contributed by Peter Mazsa, 10-Feb-2018.) |
Theorem | brinxp2ALTV 34034 | Intersection with cross product binary relation . (Contributed by NM, 3-Mar-2007.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | brres2 34035 | Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019.) (Revised by Peter Mazsa, 16-Dec-2021.) |
Theorem | eldmres 34036* | Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 9-Jan-2019.) |
Theorem | eldm4 34037* | Elementhood in a domain. (Contributed by Peter Mazsa, 24-Oct-2018.) |
Theorem | eldmres2 34038* | Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 21-Aug-2020.) |
Theorem | eceq1i 34039 | Equality theorem for -coset of and -coset of , inference version. (Contributed by Peter Mazsa, 11-May-2021.) |
Theorem | eceq2i 34040 | Equality theorem for the -coset and -coset of , inference version. (Contributed by Peter Mazsa, 11-May-2021.) |
Theorem | eceq2d 34041 | Equality theorem for the -coset and -coset of , deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.) |
Theorem | elecres 34042 | Elementhood in the restricted coset of . (Contributed by Peter Mazsa, 21-Sep-2018.) |
Theorem | ecres 34043* | Restricted coset of . (Contributed by Peter Mazsa, 9-Dec-2018.) |
Theorem | ecres2 34044 | The restricted coset of when is an element of the restriction. (Contributed by Peter Mazsa, 16-Oct-2018.) |
Theorem | eccnvepres 34045* | Restricted converse epsilon coset of . (Contributed by Peter Mazsa, 11-Feb-2018.) (Revised by Peter Mazsa, 21-Oct-2021.) |
Theorem | eleccnvep 34046 | Elementhood in the converse epsilon coset of is elementhood in . (Contributed by Peter Mazsa, 27-Jan-2019.) |
Theorem | eccnvep 34047 | The converse epsilon coset of a set is the set. (Contributed by Peter Mazsa, 27-Jan-2019.) |
Theorem | extep 34048 | Property of epsilon relation, cf. extid 34081, ~? extssr and the comment of ~? df-ssr . (Contributed by Peter Mazsa, 10-Jul-2019.) |
Theorem | eccnvepres2 34049 | The restricted converse epsilon coset of an element of the restriction is the element itself. (Contributed by Peter Mazsa, 16-Jul-2019.) |
Theorem | eccnvepres3 34050 | Condition for a restricted converse epsilon coset of a set to be the set itself. (Contributed by Peter Mazsa, 11-May-2021.) |
Theorem | eldmqsres 34051* | Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 21-Aug-2020.) |
Theorem | eldmqsres2 34052* | Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 22-Aug-2020.) |
Theorem | qsss1 34053 | Subclass theorem for quotient sets. (Contributed by Peter Mazsa, 12-Sep-2020.) |
Theorem | qseq1i 34054 | Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.) |
Theorem | qseq1d 34055 | Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.) |
Theorem | qseq2i 34056 | Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.) |
Theorem | qseq2d 34057 | Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.) |
Theorem | qseq12 34058 | Equality theorem for quotient set. (Contributed by Peter Mazsa, 17-Apr-2019.) |
Theorem | brinxprnres 34059 | Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019.) |
Theorem | inxprnres 34060* | Restriction of a class as a class of ordered pairs. (Contributed by Peter Mazsa, 2-Jan-2019.) |
Theorem | dfres4 34061 | Alternate definition of the restriction of a class. (Contributed by Peter Mazsa, 2-Jan-2019.) |
Theorem | exan3 34062* | Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.) |
Theorem | exanres 34063* | Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 2-May-2021.) |
Theorem | exanres3 34064* | Equivalent expressions with restricted existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.) |
Theorem | exanres2 34065* | Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.) |
Theorem | cnvepres 34066* | Restricted converse epsilon relation as a class of ordered pairs. (Contributed by Peter Mazsa, 10-Feb-2018.) |
Theorem | ssrel3 34067* | Subclass relation in another form when the subclass is a relation. (Contributed by Peter Mazsa, 16-Feb-2019.) |
Theorem | eqrel2 34068* | Equality of relations. (Contributed by Peter Mazsa, 8-Mar-2019.) |
Theorem | relinxp 34069 | Intersection with a Cartesian product is a relation. (Contributed by Peter Mazsa, 4-Mar-2019.) |
Theorem | rncnv 34070 | Range of converse is the domain. (Contributed by Peter Mazsa, 12-Feb-2018.) |
Theorem | dfdm6 34071* | Alternate definition of domain. (Contributed by Peter Mazsa, 2-Mar-2018.) |
Theorem | dfrn6 34072* | Alternate definition of range. (Contributed by Peter Mazsa, 1-Aug-2018.) |
Theorem | rncnvepres 34073 | The range of the restricted converse epsilon is the union of the restriction. (Contributed by Peter Mazsa, 11-Feb-2018.) (Revised by Peter Mazsa, 26-Sep-2021.) |
Theorem | dmecd 34074 | Equality of the coset of and the coset of implies equivalence of domain elementhood (equivalence is not necessary as opposed to ereldm 7790). (Contributed by Peter Mazsa, 9-Oct-2018.) |
Theorem | dmec2d 34075 | Equality of the coset of and the coset of implies equivalence of domain elementhood (equivalence is not necessary as opposed to ereldm 7790). (Contributed by Peter Mazsa, 12-Oct-2018.) |
Theorem | inxpssres 34076 | Intersection with a Cartesian product is a subclass of restriction. (Contributed by Peter Mazsa, 19-Jul-2019.) |
Theorem | brid 34077 | Property of the identity binary relation. (Contributed by Peter Mazsa, 18-Dec-2021.) |
Theorem | ideq2 34078 | For sets, the identity binary relation is the same as equality. (Contributed by Peter Mazsa, 24-Jun-2020.) (Revised by Peter Mazsa, 18-Dec-2021.) |
Theorem | idresssidinxp 34079 | Condition for the identity restriction to be a subclass of identity intersection with a Cartesian product. (Contributed by Peter Mazsa, 19-Jul-2018.) |
Theorem | idreseqidinxp 34080 | Condition for the identity restriction to be equal to the identity intersection with a Cartesian product. (Contributed by Peter Mazsa, 19-Jul-2018.) |
Theorem | extid 34081 | Property of identity relation, cf. extep 34048, ~? extssr and the comment of ~? df-ssr . (Contributed by Peter Mazsa, 5-Jul-2019.) |
Theorem | inxpss 34082* | Two ways to say that an intersection with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019.) |
Theorem | idinxpss 34083* | Two ways to say that an intersection of the identity relation with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019.) |
Theorem | inxpss3 34084* | Two ways to say that an intersection with a Cartesian product is a subclass (cf. inxpss 34082). (Contributed by Peter Mazsa, 8-Mar-2019.) |
Theorem | inxpss2 34085* | Two ways to say that intersections with Cartesian products are in a subclass relation. (Contributed by Peter Mazsa, 8-Mar-2019.) |
Theorem | inxpssidinxp 34086* | Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 34085. (Contributed by Peter Mazsa, 4-Jul-2019.) |
Theorem | idinxpssinxp 34087* | Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 34085. (Contributed by Peter Mazsa, 6-Mar-2019.) |
Theorem | idinxpres 34088 | The intersection of the identity function with a square cross product. (Contributed by FL, 2-Aug-2009.) |
Theorem | idinxpssinxp2 34089* | Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product. (Contributed by Peter Mazsa, 4-Mar-2019.) |
Theorem | idinxpssinxp3 34090 | Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product. (Contributed by Peter Mazsa, 16-Mar-2019.) |
Theorem | idinxpssinxp4 34091* | Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product (cf. idinxpssinxp2 34089). (Contributed by Peter Mazsa, 8-Mar-2019.) |
Theorem | relcnveq3 34092* | Two ways of saying a relation is symmetric. (Contributed by FL, 31-Aug-2009.) |
Theorem | relcnveq 34093 | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 23-Aug-2018.) |
Theorem | relcnveq2 34094* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019.) |
Theorem | relcnveq4 34095* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019.) |
Theorem | qsresid 34096 | Simplification of a special quotient set. (Contributed by Peter Mazsa, 2-Sep-2020.) |
Theorem | nel02 34097 | The empty set has no elements. (Contributed by Peter Mazsa, 4-Jan-2018.) |
Theorem | n0elqs 34098 | Two ways of expressing that the empty set is not an element of a quotient set. (Contributed by Peter Mazsa, 5-Dec-2019.) |
Theorem | n0elqs2 34099 | Two ways of expressing that the empty set is not an element of a quotient set. (Contributed by Peter Mazsa, 25-Jul-2021.) |
Theorem | ecex2 34100 | Condition for a coset to be a set. (Contributed by Peter Mazsa, 4-May-2019.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |