Home | Metamath
Proof Explorer Theorem List (p. 36 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 | sbcgf 3501 | Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 11-Oct-2004.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | sbc19.21g 3502 | Substitution for a variable not free in antecedent affects only the consequent. (Contributed by NM, 11-Oct-2004.) |
Theorem | sbcg 3503* | Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3501. (Contributed by Alan Sare, 10-Nov-2012.) |
Theorem | sbc2iegf 3504* | Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | sbc2ie 3505* | Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008.) (Revised by Mario Carneiro, 19-Dec-2013.) |
Theorem | sbc2iedv 3506* | Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008.) (Proof shortened by Mario Carneiro, 18-Oct-2016.) |
Theorem | sbc3ie 3507* | Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Jun-2014.) (Revised by Mario Carneiro, 29-Dec-2014.) |
Theorem | sbccomlem 3508* | Lemma for sbccom 3509. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 18-Oct-2016.) |
Theorem | sbccom 3509* | Commutative law for double class substitution. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Mario Carneiro, 18-Oct-2016.) |
Theorem | sbcralt 3510* | Interchange class substitution and restricted quantifier. (Contributed by NM, 1-Mar-2008.) (Revised by David Abernethy, 22-Feb-2010.) |
Theorem | sbcrext 3511* | Interchange class substitution and restricted existential quantifier. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.) (Revised by NM, 18-Aug-2018.) (Proof shortened by JJ, 7-Jul-2021.) |
Theorem | sbcrextOLD 3512* | Obsolete proof of sbcrext 3511 as of 7-Jul-2021. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.) (Revised by NM, 18-Aug-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | sbcralg 3513* | Interchange class substitution and restricted quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | sbcrex 3514* | Interchange class substitution and restricted existential quantifier. (Contributed by NM, 15-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
Theorem | sbcreu 3515* | Interchange class substitution and restricted uniqueness quantifier. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 18-Aug-2018.) |
Theorem | reu8nf 3516* | Restricted uniqueness using implicit substitution. This version of reu8 3402 uses a non-freeness hypothesis for and instead of distinct variable conditions. (Contributed by AV, 21-Jan-2022.) |
Theorem | sbcabel 3517* | Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005.) |
Theorem | rspsbc 3518* | Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. This provides an axiom for a predicate calculus for a restricted domain. This theorem generalizes the unrestricted stdpc4 2353 and spsbc 3448. See also rspsbca 3519 and rspcsbela 4006. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Mario Carneiro, 13-Oct-2016.) |
Theorem | rspsbca 3519* | Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. (Contributed by NM, 14-Dec-2005.) |
Theorem | rspesbca 3520* | Existence form of rspsbca 3519. (Contributed by NM, 29-Feb-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.) |
Theorem | spesbc 3521 | Existence form of spsbc 3448. (Contributed by Mario Carneiro, 18-Nov-2016.) |
Theorem | spesbcd 3522 | form of spsbc 3448. (Contributed by Mario Carneiro, 9-Feb-2017.) |
Theorem | sbcth2 3523* | A substitution into a theorem. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.) |
Theorem | ra4v 3524* | Version of ra4 3525 with a dv condition, requiring fewer axioms. This is stdpc5v 1867 for a restricted domain. (Contributed by BJ, 27-Mar-2020.) |
Theorem | ra4 3525 | Restricted quantifier version of Axiom 5 of [Mendelson] p. 69. This is the axiom stdpc5 2076 of standard predicate calculus for a restricted domain. See ra4v 3524 for a version requiring fewer axioms. (Contributed by NM, 16-Jan-2004.) (Proof shortened by BJ, 27-Mar-2020.) |
Theorem | rmo2 3526* | Alternate definition of restricted "at most one." Note that is not equivalent to (in analogy to reu6 3395); to see this, let be the empty set. However, one direction of this pattern holds; see rmo2i 3527. (Contributed by NM, 17-Jun-2017.) |
Theorem | rmo2i 3527* | Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017.) |
Theorem | rmo3 3528* | Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) |
Theorem | rmob 3529* | Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.) |
Theorem | rmoi 3530* | Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) |
Theorem | rmob2 3531* | Consequence of "restricted at most one." (Contributed by Thierry Arnoux, 9-Dec-2019.) |
Theorem | rmoi2 3532* | Consequence of "restricted at most one." (Contributed by Thierry Arnoux, 9-Dec-2019.) |
Syntax | csb 3533 | Extend class notation to include the proper substitution of a class for a set into another class. |
Definition | df-csb 3534* | Define the proper substitution of a class for a set into another class. The underlined brackets distinguish it from the substitution into a wff, wsbc 3435, to prevent ambiguity. Theorem sbcel1g 3987 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 4004 recreates substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.) |
Theorem | csb2 3535* | Alternate expression for the proper substitution into a class, without referencing substitution into a wff. Note that can be free in but cannot occur in . (Contributed by NM, 2-Dec-2013.) |
Theorem | csbeq1 3536 | Analogue of dfsbcq 3437 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Theorem | csbeq2 3537 | Substituting into equivalent classes gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.) |
Theorem | cbvcsb 3538 | Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on . (Contributed by Jeff Hankins, 13-Sep-2009.) (Revised by Mario Carneiro, 11-Dec-2016.) |
Theorem | cbvcsbv 3539* | Change the bound variable of a proper substitution into a class using implicit substitution. (Contributed by NM, 30-Sep-2008.) (Revised by Mario Carneiro, 13-Oct-2016.) |
Theorem | csbeq1d 3540 | Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.) |
Theorem | csbid 3541 | Analogue of sbid 2114 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Theorem | csbeq1a 3542 | Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Theorem | csbco 3543* | Composition law for chained substitutions into a class. (Contributed by NM, 10-Nov-2005.) |
Theorem | csbtt 3544 | Substitution doesn't affect a constant (in which is not free). (Contributed by Mario Carneiro, 14-Oct-2016.) |
Theorem | csbconstgf 3545 | Substitution doesn't affect a constant (in which is not free). (Contributed by NM, 10-Nov-2005.) |
Theorem | csbconstg 3546* | Substitution doesn't affect a constant (in which does not occur). csbconstgf 3545 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) |
Theorem | nfcsb1d 3547 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
Theorem | nfcsb1 3548 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
Theorem | nfcsb1v 3549* | Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.) |
Theorem | nfcsbd 3550 | Deduction version of nfcsb 3551. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.) |
Theorem | nfcsb 3551 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
Theorem | csbhypf 3552* | Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 3253 for class substitution version. (Contributed by NM, 19-Dec-2008.) |
Theorem | csbiebt 3553* | Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3557.) (Contributed by NM, 11-Nov-2005.) |
Theorem | csbiedf 3554* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016.) |
Theorem | csbieb 3555* | Bidirectional conversion between an implicit class substitution hypothesis and its explicit substitution equivalent. (Contributed by NM, 2-Mar-2008.) |
Theorem | csbiebg 3556* | Bidirectional conversion between an implicit class substitution hypothesis and its explicit substitution equivalent. (Contributed by NM, 24-Mar-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) |
Theorem | csbiegf 3557* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 11-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.) |
Theorem | csbief 3558* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.) |
Theorem | csbie 3559* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019.) |
Theorem | csbied 3560* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.) |
Theorem | csbied2 3561* | Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Theorem | csbie2t 3562* | Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 3563). (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 13-Oct-2016.) |
Theorem | csbie2 3563* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007.) |
Theorem | csbie2g 3564* | Conversion of implicit substitution to explicit class substitution. This version of csbie 3559 avoids a disjointness condition on and by substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016.) |
Theorem | cbvralcsf 3565 | A more general version of cbvralf 3165 that doesn't require and to be distinct from or . Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.) |
Theorem | cbvrexcsf 3566 | A more general version of cbvrexf 3166 that has no distinct variable restrictions. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.) (Proof shortened by Mario Carneiro, 7-Dec-2014.) |
Theorem | cbvreucsf 3567 | A more general version of cbvreuv 3173 that has no distinct variable restrictions. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.) |
Theorem | cbvrabcsf 3568 | A more general version of cbvrab 3198 with no distinct variable restrictions. (Contributed by Andrew Salmon, 13-Jul-2011.) |
Theorem | cbvralv2 3569* | Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.) |
Theorem | cbvrexv2 3570* | Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.) |
Syntax | cdif 3571 | Extend class notation to include class difference (read: " minus "). |
Syntax | cun 3572 | Extend class notation to include union of two classes (read: " union "). |
Syntax | cin 3573 | Extend class notation to include the intersection of two classes (read: " intersect "). |
Syntax | wss 3574 | Extend wff notation to include the subclass relation. This is read " is a subclass of " or " includes ." When exists as a set, it is also read " is a subset of ." |
Syntax | wpss 3575 | Extend wff notation with proper subclass relation. |
Theorem | difjust 3576* | Soundness justification theorem for df-dif 3577. (Contributed by Rodolfo Medina, 27-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Definition | df-dif 3577* | Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. For example, (ex-dif 27280). Contrast this operation with union (df-un 3579) and intersection (df-in 3581). Several notations are used in the literature; we chose the convention used in Definition 5.3 of [Eisenberg] p. 67 instead of the more common minus sign to reserve the latter for later use in, e.g., arithmetic. We will use the terminology " excludes " to mean . We will use " is removed from " to mean i.e. the removal of an element or equivalently the exclusion of a singleton. (Contributed by NM, 29-Apr-1994.) |
Theorem | unjust 3578* | Soundness justification theorem for df-un 3579. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Definition | df-un 3579* | Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, (ex-un 27281). Contrast this operation with difference (df-dif 3577) and intersection (df-in 3581). For an alternate definition in terms of class difference, requiring no dummy variables, see dfun2 3859. For union defined in terms of intersection, see dfun3 3865. (Contributed by NM, 23-Aug-1993.) |
Theorem | injust 3580* | Soundness justification theorem for df-in 3581. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Definition | df-in 3581* | Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, (ex-in 27282). Contrast this operation with union (df-un 3579) and difference (df-dif 3577). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 3860 and dfin4 3867. For intersection defined in terms of union, see dfin3 3866. (Contributed by NM, 29-Apr-1994.) |
Theorem | dfin5 3582* | Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.) |
Theorem | dfdif2 3583* | Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.) |
Theorem | eldif 3584 | Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.) |
Theorem | eldifd 3585 | If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3584. (Contributed by David Moews, 1-May-2017.) |
Theorem | eldifad 3586 | If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3584. (Contributed by David Moews, 1-May-2017.) |
Theorem | eldifbd 3587 | If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3584. (Contributed by David Moews, 1-May-2017.) |
Definition | df-ss 3588 | Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, (ex-ss 27284). Note that (proved in ssid 3624). Contrast this relationship with the relationship (as will be defined in df-pss 3590). For a more traditional definition, but requiring a dummy variable, see dfss2 3591. Other possible definitions are given by dfss3 3592, dfss4 3858, sspss 3706, ssequn1 3783, ssequn2 3786, sseqin2 3817, and ssdif0 3942. (Contributed by NM, 27-Apr-1994.) |
Theorem | dfss 3589 | Variant of subclass definition df-ss 3588. (Contributed by NM, 21-Jun-1993.) |
Definition | df-pss 3590 | Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, (ex-pss 27285). Note that (proved in pssirr 3707). Contrast this relationship with the relationship (as defined in df-ss 3588). Other possible definitions are given by dfpss2 3692 and dfpss3 3693. (Contributed by NM, 7-Feb-1996.) |
Theorem | dfss2 3591* | Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.) |
Theorem | dfss3 3592* | Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.) |
Theorem | dfss6 3593* | Alternate definition of subclass relationship. (Contributed by RP, 16-Apr-2020.) |
Theorem | dfss2f 3594 | Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 3-Jul-1994.) (Revised by Andrew Salmon, 27-Aug-2011.) |
Theorem | dfss3f 3595 | Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.) |
Theorem | nfss 3596 | If is not free in and , it is not free in . (Contributed by NM, 27-Dec-1996.) |
Theorem | ssel 3597 | Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) |
Theorem | ssel2 3598 | Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.) |
Theorem | sseli 3599 | Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.) |
Theorem | sselii 3600 | Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |