Home | Metamath
Proof Explorer Theorem List (p. 40 of 470) | < 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cbvrabcsf 3901 | A more general version of cbvrab 3442 with no distinct variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓} | ||
Theorem | cbvralv2 3902* | Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒) | ||
Theorem | cbvrexv2 3903* | Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒) | ||
Theorem | rspc2vd 3904* | Deduction version of 2-variable restricted specialization, using implicit substitution. Notice that the class 𝐷 for the second set variable 𝑦 may depend on the first set variable 𝑥. (Contributed by AV, 29-Mar-2021.) |
⊢ (𝑥 = 𝐴 → (𝜃 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐸) & ⊢ (𝜑 → 𝐵 ∈ 𝐸) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜃 → 𝜓)) | ||
Syntax | cdif 3905 | Extend class notation to include class difference (read: "𝐴 minus 𝐵"). |
class (𝐴 ∖ 𝐵) | ||
Syntax | cun 3906 | Extend class notation to include union of two classes (read: "𝐴 union 𝐵"). |
class (𝐴 ∪ 𝐵) | ||
Syntax | cin 3907 | Extend class notation to include the intersection of two classes (read: "𝐴 intersect 𝐵"). |
class (𝐴 ∩ 𝐵) | ||
Syntax | wss 3908 | 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 𝐵". |
wff 𝐴 ⊆ 𝐵 | ||
Syntax | wpss 3909 | Extend wff notation with proper subclass relation. |
wff 𝐴 ⊊ 𝐵 | ||
Theorem | difjust 3910* | Soundness justification theorem for df-dif 3911. (Contributed by Rodolfo Medina, 27-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)} | ||
Definition | df-dif 3911* | Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. For example, ({1, 3} ∖ {1, 8}) = {3} (ex-dif 29165). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3913) and intersection (𝐴 ∩ 𝐵) (df-in 3915). 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 3912* | Soundness justification theorem for df-un 3913. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)} | ||
Definition | df-un 3913* | Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∪ {1, 8}) = {1, 3, 8} (ex-un 29166). Contrast this operation with difference (𝐴 ∖ 𝐵) (df-dif 3911) and intersection (𝐴 ∩ 𝐵) (df-in 3915). For an alternate definition in terms of class difference, requiring no dummy variables, see dfun2 4217. For union defined in terms of intersection, see dfun3 4223. (Contributed by NM, 23-Aug-1993.) |
⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} | ||
Theorem | injust 3914* | Soundness justification theorem for df-in 3915. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} | ||
Definition | df-in 3915* | Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 29167). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3913) and difference (𝐴 ∖ 𝐵) (df-dif 3911). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4218 and dfin4 4225. For intersection defined in terms of union, see dfin3 4224. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | ||
Theorem | dfin5 3916* | Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.) |
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} | ||
Theorem | dfdif2 3917* | Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.) |
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵} | ||
Theorem | eldif 3918 | Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)) | ||
Theorem | eldifd 3919 | If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3918. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) | ||
Theorem | eldifad 3920 | If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3918. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐵) | ||
Theorem | eldifbd 3921 | If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3918. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | elneeldif 3922 | The elements of a set difference and the minuend are not equal. (Contributed by AV, 21-Oct-2023.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → 𝑋 ≠ 𝑌) | ||
Theorem | velcomp 3923 | Characterization of setvar elements of the complement of a class. (Contributed by Andrew Salmon, 15-Jul-2011.) |
⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴) | ||
Theorem | elin 3924 | Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | ||
Definition | df-ss 3925 |
Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18.
For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 29169). Note that
𝐴
⊆ 𝐴 (proved in
ssid 3964). Contrast this relationship with the
relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3927). For a more
traditional definition, but requiring a dummy variable, see dfss2 3928.
Other possible definitions are given by dfss3 3930, dfss4 4216, sspss 4057,
ssequn1 4138, ssequn2 4141, sseqin2 4173, and ssdif0 4321.
We prefer the label "ss" ("subset") for ⊆, despite the fact that it applies to classes. It is much more common to refer to this as the subset relation than subclass, especially since most of the time the arguments are in fact sets (and for pragmatic reasons we don't want to need to use different operations for sets). The way set.mm is set up, many things are technically classes despite morally (and provably) being sets, like 1 (cf. df-1 10992 and 1ex 11084) or ℝ ( cf. df-r 10994 and reex 11075). This has to do with the fact that there are no "set expressions": classes are expressions but there are only set variables in set.mm (cf. https://us.metamath.org/downloads/grammar-ambiguity.txt 11075). This is why we use ⊆ both for subclass relations and for subset relations and call it "subset". (Contributed by NM, 27-Apr-1994.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) | ||
Theorem | dfss 3926 | Variant of subclass definition df-ss 3925. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵)) | ||
Definition | df-pss 3927 | Define proper subclass (or strict subclass) relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 29170). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4058). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3925). Other possible definitions are given by dfpss2 4043 and dfpss3 4044. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | ||
Theorem | dfss2 3928* | Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.) Avoid ax-10 2137, ax-11 2154, ax-12 2171. (Revised by SN, 16-May-2024.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | dfss2OLD 3929* | Obsolete version of dfss2 3928 as of 16-May-2024. (Contributed by NM, 8-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | dfss3 3930* | Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | dfss6 3931* | Alternate definition of subclass relationship. (Contributed by RP, 16-Apr-2020.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | ||
Theorem | dfss2f 3932 | 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.) Avoid ax-13 2371. (Revised by Gino Giotto, 19-May-2023.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | dfss3f 3933 | Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | nfss 3934 | If 𝑥 is not free in 𝐴 and 𝐵, it is not free in 𝐴 ⊆ 𝐵. (Contributed by NM, 27-Dec-1996.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵 | ||
Theorem | ssel 3935 | Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) Avoid ax-12 2171. (Revised by SN, 27-May-2024.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | ||
Theorem | sselOLD 3936 | Obsolete version of ssel 3935 as of 27-May-2024. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | ||
Theorem | ssel2 3937 | Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵) | ||
Theorem | sseli 3938 | Membership implication from subclass relationship. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) | ||
Theorem | sselii 3939 | Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐶 ∈ 𝐴 ⇒ ⊢ 𝐶 ∈ 𝐵 | ||
Theorem | sselid 3940 | Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐵) | ||
Theorem | sseld 3941 | Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | ||
Theorem | sselda 3942 | Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵) | ||
Theorem | sseldd 3943 | Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐵) | ||
Theorem | ssneld 3944 | 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 3945 | 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 3946* | Inference based on subclass definition. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
Theorem | ssrd 3947 | Deduction based on subclass definition. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | ssrdv 3948* | Deduction based on subclass definition. (Contributed by NM, 15-Nov-1995.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | sstr2 3949 | Transitivity of subclass relationship. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) | ||
Theorem | sstr 3950 | Transitivity of subclass relationship. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | ||
Theorem | sstri 3951 | Subclass transitivity inference. (Contributed by NM, 5-May-2000.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | sstrd 3952 | Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sstrid 3953 | Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sstrdi 3954 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sylan9ss 3955 | A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜓 → 𝐵 ⊆ 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶) | ||
Theorem | sylan9ssr 3956 | A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜓 → 𝐵 ⊆ 𝐶) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝐴 ⊆ 𝐶) | ||
Theorem | eqss 3957 | The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 21-May-1993.) |
⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | ||
Theorem | eqssi 3958 | Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐵 ⊆ 𝐴 ⇒ ⊢ 𝐴 = 𝐵 | ||
Theorem | eqssd 3959 | Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | sssseq 3960 | If a class is a subclass of another class, then the classes are equal if and only if the other class is a subclass of the first class. (Contributed by AV, 23-Dec-2020.) |
⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | eqrd 3961 | Deduce equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 21-Mar-2017.) (Proof shortened by BJ, 1-Dec-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | eqri 3962 | Infer equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 7-Oct-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ⇒ ⊢ 𝐴 = 𝐵 | ||
Theorem | eqelssd 3963* | Equality deduction from subclass relationship and membership. (Contributed by AV, 21-Aug-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | ssid 3964 | 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 | ssidd 3965 | Weakening of ssid 3964. (Contributed by BJ, 1-Sep-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐴) | ||
Theorem | ssv 3966 | Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.) |
⊢ 𝐴 ⊆ V | ||
Theorem | sseq1 3967 | Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | ||
Theorem | sseq2 3968 | Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.) |
⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | ||
Theorem | sseq12 3969 | Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)) | ||
Theorem | sseq1i 3970 | An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) | ||
Theorem | sseq2i 3971 | An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) | ||
Theorem | sseq12i 3972 | An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷) | ||
Theorem | sseq1d 3973 | An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | ||
Theorem | sseq2d 3974 | An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | ||
Theorem | sseq12d 3975 | An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)) | ||
Theorem | eqsstri 3976 | Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | eqsstrri 3977 | Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.) |
⊢ 𝐵 = 𝐴 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | sseqtri 3978 | Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | sseqtrri 3979 | Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | eqsstrd 3980 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | eqsstrrd 3981 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sseqtrd 3982 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sseqtrrd 3983 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | 3sstr3i 3984 | 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 3985 | 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 3986 | Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ⊆ 𝐷) | ||
Theorem | 3sstr4g 3987 | 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 3988 | Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶 ⊆ 𝐷) | ||
Theorem | 3sstr4d 3989 | 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 | eqsstrid 3990 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | eqsstrrid 3991 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sseqtrdi 3992 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sseqtrrdi 3993 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sseqtrid 3994 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐵 ⊆ 𝐴 & ⊢ (𝜑 → 𝐴 = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | ||
Theorem | sseqtrrid 3995 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐵 ⊆ 𝐴 & ⊢ (𝜑 → 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | ||
Theorem | eqsstrdi 3996 | A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | eqsstrrdi 3997 | A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | eqimss 3998 | Equality implies inclusion. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | ||
Theorem | eqimss2 3999 | Equality implies inclusion. (Contributed by NM, 23-Nov-2003.) |
⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵) | ||
Theorem | eqimssi 4000 | Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 𝐴 ⊆ 𝐵 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |