P. 33 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3201-3300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	unjust 3201*	Soundness justification theorem for df-un 3202. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)}
Definition	df-un 3202*	Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. Contrast this operation with difference (𝐴 ∖ 𝐵) (df-dif 3200) and intersection (𝐴 ∩ 𝐵) (df-in 3204). (Contributed by NM, 23-Aug-1993.)
⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)}
Theorem	injust 3203*	Soundness justification theorem for df-in 3204. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
Definition	df-in 3204*	Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3202) and difference (𝐴 ∖ 𝐵) (df-dif 3200). (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
Theorem	dfin5 3205*	Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.)
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}
Theorem	dfdif2 3206*	Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.)
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵}
Theorem	eldif 3207	Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
Theorem	eldifd 3208	If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3207. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))
Theorem	eldifad 3209	If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3207. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐵)
Theorem	eldifbd 3210	If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3207. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)
2.1.12  Subclasses and subsets
Definition	df-ss 3211	Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3245). For a more traditional definition, but requiring a dummy variable, see ssalel 3213. Other possible definitions are given by dfss3 3214, ssequn1 3375, ssequn2 3378, and sseqin2 3424. (Contributed by NM, 27-Apr-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
Theorem	dfss 3212	Variant of subclass definition df-ss 3211. (Contributed by NM, 3-Sep-2004.)
⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
Theorem	ssalel 3213*	Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
Theorem	dfss3 3214*	Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	dfss2 3215	Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This is another name for df-ss 3211 which is more consistent with the naming in the Metamath Proof Explorer. (Contributed by NM, 27-Apr-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
Theorem	dfss2f 3216	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 3217	Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	nfss 3218	If 𝑥 is not free in 𝐴 and 𝐵, it is not free in 𝐴 ⊆ 𝐵. (Contributed by NM, 27-Dec-1996.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵
Theorem	ssel 3219	Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
Theorem	ssel2 3220	Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)
Theorem	sseli 3221	Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
Theorem	sselii 3222	Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐶 ∈ 𝐴    ⇒   ⊢ 𝐶 ∈ 𝐵
Theorem	sselid 3223	Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐵)
Theorem	sseld 3224	Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
Theorem	sselda 3225	Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)
Theorem	sseldd 3226	Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐵)
Theorem	ssneld 3227	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 3228	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 3229*	Inference based on subclass definition. (Contributed by NM, 5-Aug-1993.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)    ⇒   ⊢ 𝐴 ⊆ 𝐵
Theorem	ssrd 3230	Deduction based on subclass definition. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	ssrdv 3231*	Deduction based on subclass definition. (Contributed by NM, 15-Nov-1995.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	sstr2 3232	Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
Theorem	sstr 3233	Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)
Theorem	sstri 3234	Subclass transitivity inference. (Contributed by NM, 5-May-2000.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ 𝐴 ⊆ 𝐶
Theorem	sstrd 3235	Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sstrid 3236	Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sstrdi 3237	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sylan9ss 3238	A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜓 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶)
Theorem	sylan9ssr 3239	A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜓 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝐴 ⊆ 𝐶)
Theorem	eqss 3240	The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
Theorem	eqssi 3241	Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐵 ⊆ 𝐴    ⇒   ⊢ 𝐴 = 𝐵
Theorem	eqssd 3242	Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	eqrd 3243	Deduce equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 21-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	eqelssd 3244*	Equality deduction from subclass relationship and membership. (Contributed by AV, 21-Aug-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	ssid 3245	Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ 𝐴 ⊆ 𝐴
Theorem	ssidd 3246	Weakening of ssid 3245. (Contributed by BJ, 1-Sep-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐴)
Theorem	ssv 3247	Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.)
⊢ 𝐴 ⊆ V
Theorem	sseq1 3248	Equality theorem for subclasses. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
Theorem	sseq2 3249	Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
Theorem	sseq12 3250	Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
Theorem	sseq1i 3251	An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
Theorem	sseq2i 3252	An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)
Theorem	sseq12i 3253	An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)
Theorem	sseq1d 3254	An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
Theorem	sseq2d 3255	An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
Theorem	sseq12d 3256	An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
Theorem	eqsstri 3257	Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ 𝐴 ⊆ 𝐶
Theorem	eqsstrri 3258	Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.)
⊢ 𝐵 = 𝐴    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ 𝐴 ⊆ 𝐶
Theorem	sseqtri 3259	Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 ⊆ 𝐶
Theorem	sseqtrri 3260	Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 ⊆ 𝐶
Theorem	eqsstrd 3261	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	eqsstrrd 3262	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrd 3263	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrrd 3264	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	3sstr3i 3265	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 3266	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 3267	Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)
Theorem	3sstr4g 3268	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 3269	Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)
Theorem	3sstr4d 3270	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 3271	B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	eqsstrrid 3272	B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrdi 3273	A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrrdi 3274	A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrid 3275	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐵 ⊆ 𝐴    &   ⊢ (𝜑 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
Theorem	sseqtrrid 3276	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐵 ⊆ 𝐴    &   ⊢ (𝜑 → 𝐶 = 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
Theorem	eqsstrdi 3277	A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	eqsstrrdi 3278	A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	eqimss 3279	Equality implies the subclass relation. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
Theorem	eqimss2 3280	Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.)
⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵)
Theorem	eqimssi 3281	Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝐴 ⊆ 𝐵
Theorem	eqimss2i 3282	Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 ⊆ 𝐴
Theorem	nssne1 3283	Two classes are different if they don't include the same class. (Contributed by NM, 23-Apr-2015.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ⊆ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	nssne2 3284	Two classes are different if they are not subclasses of the same class. (Contributed by NM, 23-Apr-2015.)
⊢ ((𝐴 ⊆ 𝐶 ∧ ¬ 𝐵 ⊆ 𝐶) → 𝐴 ≠ 𝐵)
Theorem	nssr 3285*	Negation of subclass relationship. One direction of Exercise 13 of [TakeutiZaring] p. 18. (Contributed by Jim Kingdon, 15-Jul-2018.)
⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) → ¬ 𝐴 ⊆ 𝐵)
Theorem	nelss 3286	Demonstrate by witnesses that two classes lack a subclass relation. (Contributed by Stefan O'Rear, 5-Feb-2015.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 ⊆ 𝐶)
Theorem	ssrexf 3287	Restricted existential quantification follows from a subclass relationship. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))
Theorem	ssrmof 3288	"At most one" existential quantification restricted to a subclass. (Contributed by Thierry Arnoux, 8-Oct-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (∃*𝑥 ∈ 𝐵 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑))
Theorem	ssralv 3289*	Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)
⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))
Theorem	ssrexv 3290*	Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.)
⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))
Theorem	ralss 3291*	Restricted universal quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑)))
Theorem	rexss 3292*	Restricted existential quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑)))
Theorem	ss2ab 3293	Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994.)
⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 → 𝜓))
Theorem	abss 3294*	Class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
⊢ ({𝑥 ∣ 𝜑} ⊆ 𝐴 ↔ ∀𝑥(𝜑 → 𝑥 ∈ 𝐴))
Theorem	ssab 3295*	Subclass of a class abstraction. (Contributed by NM, 16-Aug-2006.)
⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
Theorem	ssabral 3296*	The relation for a subclass of a class abstraction is equivalent to restricted quantification. (Contributed by NM, 6-Sep-2006.)
⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	ss2abi 3297	Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}
Theorem	ss2abdv 3298*	Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})
Theorem	abssdv 3299*	Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
⊢ (𝜑 → (𝜓 → 𝑥 ∈ 𝐴))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴)
Theorem	abssi 3300*	Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    ⇒   ⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴