![]() |
Metamath
Proof Explorer Theorem List (p. 40 of 437) | < 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: | ![]() (1-28347) |
![]() (28348-29872) |
![]() (29873-43661) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ssrab 3901* | Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006.) |
⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | ssrabdv 3902* | Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 31-Aug-2006.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}) | ||
Theorem | rabssdv 3903* | Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 2-Feb-2015.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵) | ||
Theorem | ss2rabdv 3904* | Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | ss2rabi 3905 | Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabss2 3906* | Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | ssab2 3907* | Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴 | ||
Theorem | ssrab2 3908* | Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 | ||
Theorem | ssrab3 3909* | Subclass relation for a restricted class abstraction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} ⇒ ⊢ 𝐵 ⊆ 𝐴 | ||
Theorem | rabssrabd 3910* | Subclass of a restricted class abstraction. (Contributed by AV, 4-Jun-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝑥 ∈ 𝐴) → 𝜒) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | ssrabeq 3911* | 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 3912 | A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} | ||
Theorem | uniiunlem 3913* | A subset relationship useful for converting union to indexed union using dfiun2 4787 or dfiun2g 4785 and intersection to indexed intersection using dfiin2 4788. (Contributed by NM, 5-Oct-2006.) (Proof shortened by Mario Carneiro, 26-Sep-2015.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 → (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐶)) | ||
Theorem | dfpss2 3914 | Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) | ||
Theorem | dfpss3 3915 | Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴)) | ||
Theorem | psseq1 3916 | Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) | ||
Theorem | psseq2 3917 | Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)) | ||
Theorem | psseq1i 3918 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶) | ||
Theorem | psseq2i 3919 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵) | ||
Theorem | psseq12i 3920 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷) | ||
Theorem | psseq1d 3921 | An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) | ||
Theorem | psseq2d 3922 | An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)) | ||
Theorem | psseq12d 3923 | An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷)) | ||
Theorem | pssss 3924 | A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | ||
Theorem | pssne 3925 | Two classes in a proper subclass relationship are not equal. (Contributed by NM, 16-Feb-2015.) |
⊢ (𝐴 ⊊ 𝐵 → 𝐴 ≠ 𝐵) | ||
Theorem | pssssd 3926 | Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.) |
⊢ (𝜑 → 𝐴 ⊊ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | pssned 3927 | Proper subclasses are unequal. Deduction form of pssne 3925. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊊ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | sspss 3928 | Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | pssirr 3929 | Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) |
⊢ ¬ 𝐴 ⊊ 𝐴 | ||
Theorem | pssn2lp 3930 | Proper subclass has no 2-cycle loops. Compare Theorem 8 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ¬ (𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐴) | ||
Theorem | sspsstri 3931 | Two ways of stating trichotomy with respect to inclusion. (Contributed by NM, 12-Aug-2004.) |
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴)) | ||
Theorem | ssnpss 3932 | Partial trichotomy law for subclasses. (Contributed by NM, 16-May-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → ¬ 𝐵 ⊊ 𝐴) | ||
Theorem | psstr 3933 | Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) |
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐶) → 𝐴 ⊊ 𝐶) | ||
Theorem | sspsstr 3934 | Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊊ 𝐶) → 𝐴 ⊊ 𝐶) | ||
Theorem | psssstr 3935 | Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.) |
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊊ 𝐶) | ||
Theorem | psstrd 3936 | Proper subclass inclusion is transitive. Deduction form of psstr 3933. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊊ 𝐵) & ⊢ (𝜑 → 𝐵 ⊊ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐶) | ||
Theorem | sspsstrd 3937 | Transitivity involving subclass and proper subclass inclusion. Deduction form of sspsstr 3934. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊊ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐶) | ||
Theorem | psssstrd 3938 | Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr 3935. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊊ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐶) | ||
Theorem | npss 3939 | A class is not a proper subclass of another iff it satisfies a one-directional form of eqss 3836. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (¬ 𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 → 𝐴 = 𝐵)) | ||
Theorem | ssnelpss 3940 | A subclass missing a member is a proper subclass. (Contributed by NM, 12-Jan-2002.) |
⊢ (𝐴 ⊆ 𝐵 → ((𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴) → 𝐴 ⊊ 𝐵)) | ||
Theorem | ssnelpssd 3941 | Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss 3940. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐵) | ||
Theorem | ssexnelpss 3942* | If there is an element of a class which is not contained in a subclass, the subclass is a proper subclass. (Contributed by AV, 29-Jan-2020.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝑥 ∉ 𝐴) → 𝐴 ⊊ 𝐵) | ||
Theorem | dfdif3 3943* | Alternate definition of class difference. (Contributed by BJ and Jim Kingdon, 16-Jun-2022.) |
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 𝑥 ≠ 𝑦} | ||
Theorem | difeq1 3944 | Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) | ||
Theorem | difeq2 3945 | Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) | ||
Theorem | difeq12 3946 | Equality theorem for class difference. (Contributed by FL, 31-Aug-2009.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)) | ||
Theorem | difeq1i 3947 | Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶) | ||
Theorem | difeq2i 3948 | Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵) | ||
Theorem | difeq12i 3949 | Equality inference for class difference. (Contributed by NM, 29-Aug-2004.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷) | ||
Theorem | difeq1d 3950 | Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) | ||
Theorem | difeq2d 3951 | Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) | ||
Theorem | difeq12d 3952 | Equality deduction for class difference. (Contributed by FL, 29-May-2014.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)) | ||
Theorem | difeqri 3953* | Inference from membership to difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ⇒ ⊢ (𝐴 ∖ 𝐵) = 𝐶 | ||
Theorem | nfdif 3954 | Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵) | ||
Theorem | eldifi 3955 | Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵) | ||
Theorem | eldifn 3956 | Implication of membership in a class difference. (Contributed by NM, 3-May-1994.) |
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | elndif 3957 | A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.) |
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ 𝐵)) | ||
Theorem | neldif 3958 | Implication of membership in a class difference. (Contributed by NM, 28-Jun-1994.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ (𝐵 ∖ 𝐶)) → 𝐴 ∈ 𝐶) | ||
Theorem | difdif 3959 | Double class difference. Exercise 11 of [TakeutiZaring] p. 22. (Contributed by NM, 17-May-1998.) |
⊢ (𝐴 ∖ (𝐵 ∖ 𝐴)) = 𝐴 | ||
Theorem | difss 3960 | Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴 | ||
Theorem | difssd 3961 | A difference of two classes is contained in the minuend. Deduction form of difss 3960. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴) | ||
Theorem | difss2 3962 | If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → 𝐴 ⊆ 𝐵) | ||
Theorem | difss2d 3963 | If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3962. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | ssdifss 3964 | Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵) | ||
Theorem | ddif 3965 | Double complement under universal class. Exercise 4.10(s) of [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.) |
⊢ (V ∖ (V ∖ 𝐴)) = 𝐴 | ||
Theorem | ssconb 3966 | Contraposition law for subsets. (Contributed by NM, 22-Mar-1998.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ 𝐵 ⊆ (𝐶 ∖ 𝐴))) | ||
Theorem | sscon 3967 | Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) | ||
Theorem | ssdif 3968 | Difference law for subsets. (Contributed by NM, 28-May-1998.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) | ||
Theorem | ssdifd 3969 | If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is contained in (𝐵 ∖ 𝐶). Deduction form of ssdif 3968. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) | ||
Theorem | sscond 3970 | If 𝐴 is contained in 𝐵, then (𝐶 ∖ 𝐵) is contained in (𝐶 ∖ 𝐴). Deduction form of sscon 3967. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) | ||
Theorem | ssdifssd 3971 | If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is also contained in 𝐵. Deduction form of ssdifss 3964. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ 𝐵) | ||
Theorem | ssdif2d 3972 | If 𝐴 is contained in 𝐵 and 𝐶 is contained in 𝐷, then (𝐴 ∖ 𝐷) is contained in (𝐵 ∖ 𝐶). Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ (𝐵 ∖ 𝐶)) | ||
Theorem | raldifb 3973 | Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3-Jan-2018.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∉ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ (𝐴 ∖ 𝐵)𝜑) | ||
Theorem | complss 3974 | Complementation reverses inclusion. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 19-Mar-2021.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ (V ∖ 𝐴)) | ||
Theorem | compleq 3975 | Two classes are equal if and only if their complements are equal. (Contributed by BJ, 19-Mar-2021.) |
⊢ (𝐴 = 𝐵 ↔ (V ∖ 𝐴) = (V ∖ 𝐵)) | ||
Theorem | elun 3976 | Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.) |
⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)) | ||
Theorem | elunnel1 3977 | 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 3978* | Inference from membership to union. (Contributed by NM, 21-Jun-1993.) |
⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ⇒ ⊢ (𝐴 ∪ 𝐵) = 𝐶 | ||
Theorem | unidm 3979 | Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝐴 ∪ 𝐴) = 𝐴 | ||
Theorem | uncom 3980 | 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 3981 | If a class equals the union of two other classes, then it equals the union of those two classes commuted. equncom 3981 was automatically derived from equncomVD 40041 using the tools program translatewithout_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.) |
⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵)) | ||
Theorem | equncomi 3982 | Inference form of equncom 3981. equncomi 3982 was automatically derived from equncomiVD 40042 using the tools program translatewithout_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.) |
⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ 𝐴 = (𝐶 ∪ 𝐵) | ||
Theorem | uneq1 3983 | Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | ||
Theorem | uneq2 3984 | Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) | ||
Theorem | uneq12 3985 | Equality theorem for the union of two classes. (Contributed by NM, 29-Mar-1998.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | ||
Theorem | uneq1i 3986 | Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶) | ||
Theorem | uneq2i 3987 | Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵) | ||
Theorem | uneq12i 3988 | Equality inference for the union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷) | ||
Theorem | uneq1d 3989 | Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | ||
Theorem | uneq2d 3990 | Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) | ||
Theorem | uneq12d 3991 | Equality deduction for the union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | ||
Theorem | nfun 3992 | Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵) | ||
Theorem | unass 3993 | 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 3994 | A rearrangement of union. (Contributed by NM, 12-Aug-2004.) |
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (𝐴 ∪ 𝐶)) | ||
Theorem | un23 3995 | A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ 𝐵) | ||
Theorem | un4 3996 | A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.) |
⊢ ((𝐴 ∪ 𝐵) ∪ (𝐶 ∪ 𝐷)) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐷)) | ||
Theorem | unundi 3997 | Union distributes over itself. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∪ (𝐴 ∪ 𝐶)) | ||
Theorem | unundir 3998 | Union distributes over itself. (Contributed by NM, 17-Aug-2004.) |
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐶)) | ||
Theorem | ssun1 3999 | Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) | ||
Theorem | ssun2 4000 | Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |