P. 32 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3101-3200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	csbidmg 3101*	Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
Theorem	sbcco3g 3102*	Composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜑))
Theorem	csbco3g 3103*	Composition of two class substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐷)
Theorem	rspcsbela 3104*	Special case related to rspsbc 3033. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)
Theorem	sbnfc2 3105*	Two ways of expressing "𝑥 is (effectively) not free in 𝐴." (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴)
Theorem	csbabg 3106*	Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} = {𝑦 ∣ [𝐴 / 𝑥]𝜑})
Theorem	cbvralcsf 3107	A more general version of cbvralf 2685 that doesn't require 𝐴 and 𝐵 to be distinct from 𝑥 or 𝑦. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrexcsf 3108	A more general version of cbvrexf 2686 that has no distinct variable restrictions. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.) (Proof shortened by Mario Carneiro, 7-Dec-2014.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
Theorem	cbvreucsf 3109	A more general version of cbvreuv 2694 that has no distinct variable rextrictions. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrabcsf 3110	A more general version of cbvrab 2724 with no distinct variable restrictions. (Contributed by Andrew Salmon, 13-Jul-2011.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓}
Theorem	cbvralv2 3111*	Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)
Theorem	cbvrexv2 3112*	Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)
2.1.11  Define basic set operations and relations
Syntax	cdif 3113	Extend class notation to include class difference (read: "𝐴 minus 𝐵").
class (𝐴 ∖ 𝐵)
Syntax	cun 3114	Extend class notation to include union of two classes (read: "𝐴 union 𝐵").
class (𝐴 ∪ 𝐵)
Syntax	cin 3115	Extend class notation to include the intersection of two classes (read: "𝐴 intersect 𝐵").
class (𝐴 ∩ 𝐵)
Syntax	wss 3116	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 𝐴 ⊆ 𝐵
Theorem	difjust 3117*	Soundness justification theorem for df-dif 3118. (Contributed by Rodolfo Medina, 27-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)}
Definition	df-dif 3118*	Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3120) and intersection (𝐴 ∩ 𝐵) (df-in 3122). 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 3119*	Soundness justification theorem for df-un 3120. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)}
Definition	df-un 3120*	Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. Contrast this operation with difference (𝐴 ∖ 𝐵) (df-dif 3118) and intersection (𝐴 ∩ 𝐵) (df-in 3122). (Contributed by NM, 23-Aug-1993.)
⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)}
Theorem	injust 3121*	Soundness justification theorem for df-in 3122. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
Definition	df-in 3122*	Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3120) and difference (𝐴 ∖ 𝐵) (df-dif 3118). (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
Theorem	dfin5 3123*	Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.)
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}
Theorem	dfdif2 3124*	Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.)
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵}
Theorem	eldif 3125	Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
Theorem	eldifd 3126	If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3125. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))
Theorem	eldifad 3127	If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3125. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐵)
Theorem	eldifbd 3128	If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3125. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)
2.1.12  Subclasses and subsets
Definition	df-ss 3129	Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3162). For a more traditional definition, but requiring a dummy variable, see dfss2 3131. Other possible definitions are given by dfss3 3132, ssequn1 3292, ssequn2 3295, and sseqin2 3341. (Contributed by NM, 27-Apr-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
Theorem	dfss 3130	Variant of subclass definition df-ss 3129. (Contributed by NM, 3-Sep-2004.)
⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
Theorem	dfss2 3131*	Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
Theorem	dfss3 3132*	Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	dfss2f 3133	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 3134	Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	nfss 3135	If 𝑥 is not free in 𝐴 and 𝐵, it is not free in 𝐴 ⊆ 𝐵. (Contributed by NM, 27-Dec-1996.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵
Theorem	ssel 3136	Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
Theorem	ssel2 3137	Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)
Theorem	sseli 3138	Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
Theorem	sselii 3139	Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐶 ∈ 𝐴    ⇒   ⊢ 𝐶 ∈ 𝐵
Theorem	sselid 3140	Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐵)
Theorem	sseld 3141	Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
Theorem	sselda 3142	Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)
Theorem	sseldd 3143	Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐵)
Theorem	ssneld 3144	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 3145	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 3146*	Inference based on subclass definition. (Contributed by NM, 5-Aug-1993.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)    ⇒   ⊢ 𝐴 ⊆ 𝐵
Theorem	ssrd 3147	Deduction based on subclass definition. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	ssrdv 3148*	Deduction based on subclass definition. (Contributed by NM, 15-Nov-1995.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	sstr2 3149	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 3150	Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)
Theorem	sstri 3151	Subclass transitivity inference. (Contributed by NM, 5-May-2000.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ 𝐴 ⊆ 𝐶
Theorem	sstrd 3152	Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sstrid 3153	Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sstrdi 3154	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sylan9ss 3155	A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜓 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶)
Theorem	sylan9ssr 3156	A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜓 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝐴 ⊆ 𝐶)
Theorem	eqss 3157	The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
Theorem	eqssi 3158	Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐵 ⊆ 𝐴    ⇒   ⊢ 𝐴 = 𝐵
Theorem	eqssd 3159	Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	eqrd 3160	Deduce equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 21-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	eqelssd 3161*	Equality deduction from subclass relationship and membership. (Contributed by AV, 21-Aug-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	ssid 3162	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 3163	Weakening of ssid 3162. (Contributed by BJ, 1-Sep-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐴)
Theorem	ssv 3164	Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.)
⊢ 𝐴 ⊆ V
Theorem	sseq1 3165	Equality theorem for subclasses. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
Theorem	sseq2 3166	Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
Theorem	sseq12 3167	Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
Theorem	sseq1i 3168	An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
Theorem	sseq2i 3169	An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)
Theorem	sseq12i 3170	An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)
Theorem	sseq1d 3171	An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
Theorem	sseq2d 3172	An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
Theorem	sseq12d 3173	An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
Theorem	eqsstri 3174	Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ 𝐴 ⊆ 𝐶
Theorem	eqsstrri 3175	Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.)
⊢ 𝐵 = 𝐴    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ 𝐴 ⊆ 𝐶
Theorem	sseqtri 3176	Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 ⊆ 𝐶
Theorem	sseqtrri 3177	Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 ⊆ 𝐶
Theorem	eqsstrd 3178	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	eqsstrrd 3179	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrd 3180	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrrd 3181	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	3sstr3i 3182	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 3183	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 3184	Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)
Theorem	3sstr4g 3185	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 3186	Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)
Theorem	3sstr4d 3187	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 3188	B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	eqsstrrid 3189	B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrdi 3190	A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrrdi 3191	A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sseqtrid 3192	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐵 ⊆ 𝐴    &   ⊢ (𝜑 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
Theorem	sseqtrrid 3193	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐵 ⊆ 𝐴    &   ⊢ (𝜑 → 𝐶 = 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
Theorem	eqsstrdi 3194	A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	eqsstrrdi 3195	A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	eqimss 3196	Equality implies the subclass relation. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
Theorem	eqimss2 3197	Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.)
⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵)
Theorem	eqimssi 3198	Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝐴 ⊆ 𝐵
Theorem	eqimss2i 3199	Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 ⊆ 𝐴
Theorem	nssne1 3200	Two classes are different if they don't include the same class. (Contributed by NM, 23-Apr-2015.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ⊆ 𝐶) → 𝐵 ≠ 𝐶)