P. 40 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 3901-4000   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-dif 3901*	Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. For example, ({1, 3} ∖ {1, 8}) = {3} (ex-dif 30958). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3903) and intersection (𝐴 ∩ 𝐵) (df-in 3905). 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 3902*	Soundness justification theorem for df-un 3903. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)}
Definition	df-un 3903*	Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∪ {1, 8}) = {1, 3, 8} (ex-un 30959). Contrast this operation with difference (𝐴 ∖ 𝐵) (df-dif 3901) and intersection (𝐴 ∩ 𝐵) (df-in 3905). For an alternate definition in terms of class difference, requiring no dummy variables, see dfun2 4215. For union defined in terms of intersection, see dfun3 4221. (Contributed by NM, 23-Aug-1993.)
⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)}
Theorem	injust 3904*	Soundness justification theorem for df-in 3905. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
Definition	df-in 3905*	Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 30960). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3903) and difference (𝐴 ∖ 𝐵) (df-dif 3901). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4216 and dfin4 4223. For intersection defined in terms of union, see dfin3 4222. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
Theorem	dfin5 3906*	Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.)
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}
Theorem	dfdif2 3907*	Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.)
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵}
Theorem	eldif 3908	Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
Theorem	eldifd 3909	If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3908. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))
Theorem	eldifad 3910	If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3908. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐵)
Theorem	eldifbd 3911	If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3908. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)
Theorem	elneeldif 3912	The elements of a set difference and the minuend are not equal. (Contributed by AV, 21-Oct-2023.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → 𝑋 ≠ 𝑌)
Theorem	velcomp 3913	Characterization of setvar elements of the complement of a class. (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴)
Theorem	elin 3914	Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2.1.12  Subclasses and subsets
Definition	df-ss 3915*	Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30962). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3952). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3918). For an alternative definition, not requiring a dummy variable, see dfss2 3916. Other possible definitions are given by dfss3 3919, dfss4 4214, sspss 4049, ssequn1 4131, ssequn2 4134, sseqin2 4168, and ssdif0 4313. 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 11180 and 1ex 11275) or ℝ ( cf. df-r 11182 and reex 11263). 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 11263). This is why we use ⊆ both for subclass relations and for subset relations and call it "subset". (Contributed by NM, 8-Jan-2002.) Revised from the original definition dfss2 3916. (Revised by GG, 15-May-2025.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
Theorem	dfss2 3916	Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3915. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3915. (Revised by GG, 15-May-2025.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
Theorem	dfss 3917	Variant of subclass definition dfss2 3916. (Contributed by NM, 21-Jun-1993.)
⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
Definition	df-pss 3918	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 30963). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4050). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3915). Other possible definitions are given by dfpss2 4035 and dfpss3 4036. (Contributed by NM, 7-Feb-1996.)
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
Theorem	dfss3 3919*	Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	dfss6 3920*	Alternate definition of subclass relationship. (Contributed by RP, 16-Apr-2020.)
⊢ (𝐴 ⊆ 𝐵 ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
Theorem	dfssf 3921	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 2401. (Revised by GG, 19-May-2023.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
Theorem	dfss3f 3922	Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	nfss 3923	If 𝑥 is not free in 𝐴 and 𝐵, it is not free in 𝐴 ⊆ 𝐵. (Contributed by NM, 27-Dec-1996.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵
Theorem	ssel 3924	Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) Avoid ax-12 2213. (Revised by SN, 27-May-2024.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
Theorem	ssel2 3925	Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)
Theorem	sseli 3926	Membership implication from subclass relationship. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
Theorem	sselii 3927	Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐶 ∈ 𝐴    ⇒   ⊢ 𝐶 ∈ 𝐵
Theorem	sselid 3928	Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐵)
Theorem	sseld 3929	Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
Theorem	sselda 3930	Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)
Theorem	sseldd 3931	Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐵)
Theorem	ssneld 3932	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 3933	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 3934*	Inference based on subclass definition. (Contributed by NM, 21-Jun-1993.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)    ⇒   ⊢ 𝐴 ⊆ 𝐵
Theorem	ssrd 3935	Deduction based on subclass definition. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	ssrdv 3936*	Deduction based on subclass definition. (Contributed by NM, 15-Nov-1995.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	sstr2 3937	Transitivity of subclass relationship. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) Avoid axioms. (Revised by GG, 19-May-2025.)
⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
Theorem	sstr 3938	Transitivity of subclass relationship. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)
Theorem	sstri 3939	Subclass transitivity inference. (Contributed by NM, 5-May-2000.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ 𝐴 ⊆ 𝐶
Theorem	sstrd 3940	Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sstrid 3941	Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sstrdi 3942	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sylan9ss 3943	A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜓 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶)
Theorem	sylan9ssr 3944	A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜓 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝐴 ⊆ 𝐶)
Theorem	eqss 3945	The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 21-May-1993.)
⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
Theorem	eqssi 3946	Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐵 ⊆ 𝐴    ⇒   ⊢ 𝐴 = 𝐵
Theorem	eqssd 3947	Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	sssseq 3948	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 3949	Deduce equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 21-Mar-2017.) (Proof shortened by BJ, 1-Dec-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	eqri 3950	Infer equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 7-Oct-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)    ⇒   ⊢ 𝐴 = 𝐵
Theorem	eqelssd 3951*	Equality deduction from subclass relationship and membership. (Contributed by AV, 21-Aug-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	ssid 3952	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 3953	Weakening of ssid 3952. (Contributed by BJ, 1-Sep-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐴)
Theorem	ssv 3954	Any class is a subclass of the universal class. Dual of 0ss 4349. (Contributed by NM, 31-Oct-1995.)
⊢ 𝐴 ⊆ V
Theorem	sseq1 3955	Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
Theorem	sseq2 3956	Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
Theorem	sseq12 3957	Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
Theorem	sseq1i 3958	An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
Theorem	sseq2i 3959	An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)
Theorem	sseq12i 3960	An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)
Theorem	sseq1d 3961	An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
Theorem	sseq2d 3962	An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
Theorem	sseq12d 3963	An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
Theorem	eqsstrd 3964	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	eqsstrrd 3965	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrd 3966	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrrd 3967	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	eqsstrid 3968	A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	eqsstrrid 3969	A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrdi 3970	A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrrdi 3971	A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrid 3972	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐵 ⊆ 𝐴    &   ⊢ (𝜑 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
Theorem	sseqtrrid 3973	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐵 ⊆ 𝐴    &   ⊢ (𝜑 → 𝐶 = 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
Theorem	eqsstrdi 3974	A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	eqsstrrdi 3975	A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
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	3sstr3i 3980	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 3981	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 3982	Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)
Theorem	3sstr4g 3983	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 3984	Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)
Theorem	3sstr4d 3985	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	eqimssd 3986	Equality implies inclusion, deduction version. (Contributed by SN, 6-Nov-2024.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	eqimsscd 3987	Equality implies inclusion, deduction version. (Contributed by SN, 15-Feb-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
Theorem	eqimss 3988	Equality implies inclusion. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
Theorem	eqimss2 3989	Equality implies inclusion. (Contributed by NM, 23-Nov-2003.)
⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵)
Theorem	eqimssi 3990	Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝐴 ⊆ 𝐵
Theorem	eqimss2i 3991	Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 ⊆ 𝐴
Theorem	nssne1 3992	Two classes are different if they don't include the same class. (Contributed by NM, 23-Apr-2015.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ⊆ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	nssne2 3993	Two classes are different if they are not subclasses of the same class. (Contributed by NM, 23-Apr-2015.)
⊢ ((𝐴 ⊆ 𝐶 ∧ ¬ 𝐵 ⊆ 𝐶) → 𝐴 ≠ 𝐵)
Theorem	nss 3994*	Negation of subclass relationship. Exercise 13 of [TakeutiZaring] p. 18. (Contributed by NM, 25-Feb-1996.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
Theorem	nssrex 3995*	Negation of subclass relationship. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)
Theorem	nelss 3996	Demonstrate by witnesses that two classes lack a subclass relation. (Contributed by Stefan O'Rear, 5-Feb-2015.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 ⊆ 𝐶)
Theorem	ssrexf 3997	Restricted existential quantification follows from a subclass relationship. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))
Theorem	ssrmof 3998	"At most one" existential quantification restricted to a subclass. (Contributed by Thierry Arnoux, 8-Oct-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (∃*𝑥 ∈ 𝐵 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑))
Theorem	ssralv 3999*	Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.) Avoid axioms. (Revised by GG, 19-May-2025.)
⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))
Theorem	ssrexv 4000*	Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.) Avoid axioms. (Revised by GG, 19-May-2025.)
⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))