Home | Metamath
Proof Explorer Theorem List (p. 38 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | difss2 3701 | If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → 𝐴 ⊆ 𝐵) | ||
Theorem | difss2d 3702 | If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3701. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | ssdifss 3703 | Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵) | ||
Theorem | ddif 3704 | Double complement under universal class. Exercise 4.10(s) of [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.) |
⊢ (V ∖ (V ∖ 𝐴)) = 𝐴 | ||
Theorem | ssconb 3705 | Contraposition law for subsets. (Contributed by NM, 22-Mar-1998.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ 𝐵 ⊆ (𝐶 ∖ 𝐴))) | ||
Theorem | sscon 3706 | Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) | ||
Theorem | ssdif 3707 | Difference law for subsets. (Contributed by NM, 28-May-1998.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) | ||
Theorem | ssdifd 3708 | If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is contained in (𝐵 ∖ 𝐶). Deduction form of ssdif 3707. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) | ||
Theorem | sscond 3709 | If 𝐴 is contained in 𝐵, then (𝐶 ∖ 𝐵) is contained in (𝐶 ∖ 𝐴). Deduction form of sscon 3706. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) | ||
Theorem | ssdifssd 3710 | If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is also contained in 𝐵. Deduction form of ssdifss 3703. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ 𝐵) | ||
Theorem | ssdif2d 3711 | If 𝐴 is contained in 𝐵 and 𝐶 is contained in 𝐷, then (𝐴 ∖ 𝐷) is contained in (𝐵 ∖ 𝐶). Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ (𝐵 ∖ 𝐶)) | ||
Theorem | raldifb 3712 | Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3-Jan-2018.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∉ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ (𝐴 ∖ 𝐵)𝜑) | ||
Theorem | complss 3713 | Complementation reverses inclusion. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 19-Mar-2021.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ (V ∖ 𝐴)) | ||
Theorem | compleq 3714 | Two classes are equal if and only if their complements are equal. (Contributed by BJ, 19-Mar-2021.) |
⊢ (𝐴 = 𝐵 ↔ (V ∖ 𝐴) = (V ∖ 𝐵)) | ||
Theorem | elun 3715 | Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.) |
⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)) | ||
Theorem | elunnel1 3716 | A member of a union that is not member of the first class, is member of the second class. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ (𝐵 ∪ 𝐶) ∧ ¬ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐶) | ||
Theorem | uneqri 3717* | Inference from membership to union. (Contributed by NM, 21-Jun-1993.) |
⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ⇒ ⊢ (𝐴 ∪ 𝐵) = 𝐶 | ||
Theorem | unidm 3718 | Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝐴 ∪ 𝐴) = 𝐴 | ||
Theorem | uncom 3719 | Commutative law for union of classes. Exercise 6 of [TakeutiZaring] p. 17. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴) | ||
Theorem | equncom 3720 | If a class equals the union of two other classes, then it equals the union of those two classes commuted. equncom 3720 was automatically derived from equncomVD 38126 using the tools program translatewithout_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.) |
⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵)) | ||
Theorem | equncomi 3721 | Inference form of equncom 3720. equncomi 3721 was automatically derived from equncomiVD 38127 using the tools program translatewithout_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.) |
⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ 𝐴 = (𝐶 ∪ 𝐵) | ||
Theorem | uneq1 3722 | Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | ||
Theorem | uneq2 3723 | Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) | ||
Theorem | uneq12 3724 | Equality theorem for the union of two classes. (Contributed by NM, 29-Mar-1998.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | ||
Theorem | uneq1i 3725 | Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶) | ||
Theorem | uneq2i 3726 | Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵) | ||
Theorem | uneq12i 3727 | Equality inference for the union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷) | ||
Theorem | uneq1d 3728 | Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | ||
Theorem | uneq2d 3729 | Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) | ||
Theorem | uneq12d 3730 | Equality deduction for the union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | ||
Theorem | nfun 3731 | Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵) | ||
Theorem | unass 3732 | Associative law for union of classes. Exercise 8 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵 ∪ 𝐶)) | ||
Theorem | un12 3733 | A rearrangement of union. (Contributed by NM, 12-Aug-2004.) |
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (𝐴 ∪ 𝐶)) | ||
Theorem | un23 3734 | A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ 𝐵) | ||
Theorem | un4 3735 | A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.) |
⊢ ((𝐴 ∪ 𝐵) ∪ (𝐶 ∪ 𝐷)) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐷)) | ||
Theorem | unundi 3736 | Union distributes over itself. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∪ (𝐴 ∪ 𝐶)) | ||
Theorem | unundir 3737 | Union distributes over itself. (Contributed by NM, 17-Aug-2004.) |
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐶)) | ||
Theorem | ssun1 3738 | Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) | ||
Theorem | ssun2 3739 | Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴) | ||
Theorem | ssun3 3740 | Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐵 ∪ 𝐶)) | ||
Theorem | ssun4 3741 | Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.) |
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐶 ∪ 𝐵)) | ||
Theorem | elun1 3742 | Membership law for union of classes. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶)) | ||
Theorem | elun2 3743 | Membership law for union of classes. (Contributed by NM, 30-Aug-1993.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵)) | ||
Theorem | unss1 3744 | Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶)) | ||
Theorem | ssequn1 3745 | A relationship between subclass and union. Theorem 26 of [Suppes] p. 27. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) | ||
Theorem | unss2 3746 | Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18. (Contributed by NM, 14-Oct-1999.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∪ 𝐴) ⊆ (𝐶 ∪ 𝐵)) | ||
Theorem | unss12 3747 | Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷)) | ||
Theorem | ssequn2 3748 | A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵) | ||
Theorem | unss 3749 | The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse. (Contributed by NM, 11-Jun-2004.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | ||
Theorem | unssi 3750 | An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 𝐴 ⊆ 𝐶 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶 | ||
Theorem | unssd 3751 | A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) | ||
Theorem | unssad 3752 | If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 3749. Partial converse of unssd 3751. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | unssbd 3753 | If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 3749. Partial converse of unssd 3751. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | ||
Theorem | ssun 3754 | A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003.) |
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶) → 𝐴 ⊆ (𝐵 ∪ 𝐶)) | ||
Theorem | rexun 3755 | Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | ralunb 3756 | Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | ralun 3757 | Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑) | ||
Theorem | elin 3758 | Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | ||
Theorem | elini 3759 | Membership in an intersection of two classes. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ 𝐴 ∈ (𝐵 ∩ 𝐶) | ||
Theorem | elind 3760 | Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) | ||
Theorem | elinel1 3761 | Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵) | ||
Theorem | elinel2 3762 | Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶) | ||
Theorem | elin2 3763 | Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑋 = (𝐵 ∩ 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | ||
Theorem | elin1d 3764 | Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.) |
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐴) | ||
Theorem | elin2d 3765 | Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.) |
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐵) | ||
Theorem | elin3 3766 | Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑋 = ((𝐵 ∩ 𝐶) ∩ 𝐷) ⇒ ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ 𝐷)) | ||
Theorem | incom 3767 | Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) | ||
Theorem | ineqri 3768* | Inference from membership to intersection. (Contributed by NM, 21-Jun-1993.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ⇒ ⊢ (𝐴 ∩ 𝐵) = 𝐶 | ||
Theorem | ineq1 3769 | Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | ||
Theorem | ineq2 3770 | Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) | ||
Theorem | ineq12 3771 | Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | ||
Theorem | ineq1i 3772 | Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶) | ||
Theorem | ineq2i 3773 | Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵) | ||
Theorem | ineq12i 3774 | Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷) | ||
Theorem | ineq1d 3775 | Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | ||
Theorem | ineq2d 3776 | Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) | ||
Theorem | ineq12d 3777 | Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | ||
Theorem | ineqan12d 3778 | Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | ||
Theorem | sseqin2 3779 | A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) | ||
Theorem | dfss1OLD 3780 | Obsolete as of 22-Jul-2021. (Contributed by NM, 10-Jan-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) | ||
Theorem | dfss5OLD 3781 | Obsolete as of 22-Jul-2021. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐵 ∩ 𝐴)) | ||
Theorem | nfin 3782 | Bound-variable hypothesis builder for the intersection of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵) | ||
Theorem | rabbi2dva 3783* | Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝜓}) | ||
Theorem | inidm 3784 | Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 ∩ 𝐴) = 𝐴 | ||
Theorem | inass 3785 | Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶)) | ||
Theorem | in12 3786 | A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) |
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐵 ∩ (𝐴 ∩ 𝐶)) | ||
Theorem | in32 3787 | A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ 𝐵) | ||
Theorem | in13 3788 | A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.) |
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐶 ∩ (𝐵 ∩ 𝐴)) | ||
Theorem | in31 3789 | A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐵) ∩ 𝐴) | ||
Theorem | inrot 3790 | Rotate the intersection of 3 classes. (Contributed by NM, 27-Aug-2012.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐴) ∩ 𝐵) | ||
Theorem | in4 3791 | Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001.) |
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐷)) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐷)) | ||
Theorem | inindi 3792 | Intersection distributes over itself. (Contributed by NM, 6-May-1994.) |
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = ((𝐴 ∩ 𝐵) ∩ (𝐴 ∩ 𝐶)) | ||
Theorem | inindir 3793 | Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶)) | ||
Theorem | sseqin2OLD 3794 | Obsolete proof of sseqin2 3779 as of 22-Jul-2021. (Contributed by NM, 17-May-1994.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) | ||
Theorem | inss1 3795 | The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.) |
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 | ||
Theorem | inss2 3796 | The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.) |
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 | ||
Theorem | ssin 3797 | Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26. (Contributed by NM, 15-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶)) | ||
Theorem | ssini 3798 | An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐴 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶) | ||
Theorem | ssind 3799 | A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶)) | ||
Theorem | ssrin 3800 | Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |