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
Theorem	csb2 3901*	Alternate expression for the proper substitution into a class, without referencing substitution into a wff. Note that 𝑥 can be free in 𝐵 but cannot occur in 𝐴. (Contributed by NM, 2-Dec-2013.)
⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ ∃𝑥(𝑥 = 𝐴 ∧ 𝑦 ∈ 𝐵)}
Theorem	csbeq1 3902	Analogue of dfsbcq 3790 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)
Theorem	csbeq1d 3903	Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)
Theorem	csbeq2 3904	Substituting into equivalent classes gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
⊢ (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2d 3905	Formula-building deduction for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2dv 3906*	Formula-building deduction for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2i 3907	Formula-building inference for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶
Theorem	csbeq12dv 3908*	Formula-building inference for class substitution. (Contributed by SN, 3-Nov-2023.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐷)
Theorem	cbvcsbw 3909*	Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on 𝐴. Version of cbvcsb 3910 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by Jeff Hankins, 13-Sep-2009.) Avoid ax-13 2377. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑦⦌𝐷
Theorem	cbvcsb 3910	Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on 𝐴. Usage of this theorem is discouraged because it depends on ax-13 2377. Use the weaker cbvcsbw 3909 when possible. (Contributed by Jeff Hankins, 13-Sep-2009.) (Revised by Mario Carneiro, 11-Dec-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑦⦌𝐷
Theorem	cbvcsbv 3911*	Change the bound variable of a proper substitution into a class using implicit substitution. (Contributed by NM, 30-Sep-2008.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑦⦌𝐶
Theorem	csbid 3912	Analogue of sbid 2255 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴
Theorem	csbeq1a 3913	Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
Theorem	csbcow 3914*	Composition law for chained substitutions into a class. Version of csbco 3915 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by NM, 10-Nov-2005.) Avoid ax-13 2377. (Revised by GG, 10-Jan-2024.)
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵
Theorem	csbco 3915*	Composition law for chained substitutions into a class. Usage of this theorem is discouraged because it depends on ax-13 2377. Use the weaker csbcow 3914 when possible. (Contributed by NM, 10-Nov-2005.) (New usage is discouraged.)
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵
Theorem	csbtt 3916	Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐵) → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)
Theorem	csbconstgf 3917	Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by NM, 10-Nov-2005.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)
Theorem	csbconstg 3918*	Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3917 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2177. (Revised by GG, 15-Oct-2024.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)
Theorem	csbgfi 3919	Substitution for a variable not free in a class does not affect it, in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵
Theorem	csbconstgi 3920*	The proper substitution of a class for a variable in another variable does not modify it, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝑦 = 𝑦
Theorem	nfcsb1d 3921	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵)
Theorem	nfcsb1 3922	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵
Theorem	nfcsb1v 3923*	Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵
Theorem	nfcsbd 3924	Deduction version of nfcsb 3926. Usage of this theorem is discouraged because it depends on ax-13 2377. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵)
Theorem	nfcsbw 3925*	Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3926 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by Mario Carneiro, 12-Oct-2016.) Avoid ax-13 2377. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵
Theorem	nfcsb 3926	Bound-variable hypothesis builder for substitution into a class. Usage of this theorem is discouraged because it depends on ax-13 2377. Use the weaker nfcsbw 3925 when possible. (Contributed by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵
Theorem	csbhypf 3927*	Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 3544 for class substitution version. (Contributed by NM, 19-Dec-2008.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbiebt 3928*	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3932.) (Contributed by NM, 11-Nov-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶))
Theorem	csbiedf 3929*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbieb 3930*	Bidirectional conversion between an implicit class substitution hypothesis 𝑥 = 𝐴 → 𝐵 = 𝐶 and its explicit substitution equivalent. (Contributed by NM, 2-Mar-2008.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbiebg 3931*	Bidirectional conversion between an implicit class substitution hypothesis 𝑥 = 𝐴 → 𝐵 = 𝐶 and its explicit substitution equivalent. (Contributed by NM, 24-Mar-2013.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶))
Theorem	csbiegf 3932*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 11-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ (𝐴 ∈ 𝑉 → Ⅎ𝑥𝐶)    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbief 3933*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶
Theorem	csbie 3934*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019.) Reduce axiom usage. (Revised by GG, 15-Oct-2024.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶
Theorem	csbied 3935*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.) Reduce axiom usage. (Revised by GG, 15-Oct-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbied2 3936*	Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷)
Theorem	csbie2t 3937*	Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 3938). (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷)
Theorem	csbie2 3938*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷
Theorem	csbie2g 3939*	Conversion of implicit substitution to explicit class substitution. This version of csbie 3934 avoids a disjointness condition on 𝑥, 𝐴 and 𝑥, 𝐷 by substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    &   ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷)
Theorem	cbvrabcsfw 3940*	Version of cbvrabcsf 3944 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by Andrew Salmon, 13-Jul-2011.) (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓}
Theorem	cbvralcsf 3941	A more general version of cbvralf 3360 that doesn't require 𝐴 and 𝐵 to be distinct from 𝑥 or 𝑦. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2377. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrexcsf 3942	A more general version of cbvrexf 3361 that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2377. (Contributed by Andrew Salmon, 13-Jul-2011.) (Proof shortened by Mario Carneiro, 7-Dec-2014.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
Theorem	cbvreucsf 3943	A more general version of cbvreuv 3431 that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2377. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrabcsf 3944	A more general version of cbvrab 3479 with no distinct variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2377. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓}
Theorem	cbvralv2 3945*	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 2377. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)
Theorem	cbvrexv2 3946*	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 2377. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)
Theorem	rspc2vd 3947*	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.)
⊢ (𝑥 = 𝐴 → (𝜃 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐸)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐸)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜃 → 𝜓))
2.1.11  Define basic set operations and relations
Syntax	cdif 3948	Extend class notation to include class difference (read: "𝐴 minus 𝐵").
class (𝐴 ∖ 𝐵)
Syntax	cun 3949	Extend class notation to include union of two classes (read: "𝐴 union 𝐵").
class (𝐴 ∪ 𝐵)
Syntax	cin 3950	Extend class notation to include the intersection of two classes (read: "𝐴 intersect 𝐵").
class (𝐴 ∩ 𝐵)
Syntax	wss 3951	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 3952	Extend wff notation with proper subclass relation.
wff 𝐴 ⊊ 𝐵
Theorem	difjust 3953*	Soundness justification theorem for df-dif 3954. (Contributed by Rodolfo Medina, 27-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)}
Definition	df-dif 3954*	Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. For example, ({1, 3} ∖ {1, 8}) = {3} (ex-dif 30442). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3956) and intersection (𝐴 ∩ 𝐵) (df-in 3958). 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 3955*	Soundness justification theorem for df-un 3956. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)}
Definition	df-un 3956*	Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∪ {1, 8}) = {1, 3, 8} (ex-un 30443). Contrast this operation with difference (𝐴 ∖ 𝐵) (df-dif 3954) and intersection (𝐴 ∩ 𝐵) (df-in 3958). For an alternate definition in terms of class difference, requiring no dummy variables, see dfun2 4270. For union defined in terms of intersection, see dfun3 4276. (Contributed by NM, 23-Aug-1993.)
⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)}
Theorem	injust 3957*	Soundness justification theorem for df-in 3958. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
Definition	df-in 3958*	Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 30444). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3956) and difference (𝐴 ∖ 𝐵) (df-dif 3954). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4271 and dfin4 4278. For intersection defined in terms of union, see dfin3 4277. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
Theorem	dfin5 3959*	Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.)
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}
Theorem	dfdif2 3960*	Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.)
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵}
Theorem	eldif 3961	Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
Theorem	eldifd 3962	If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3961. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))
Theorem	eldifad 3963	If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3961. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐵)
Theorem	eldifbd 3964	If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3961. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)
Theorem	elneeldif 3965	The elements of a set difference and the minuend are not equal. (Contributed by AV, 21-Oct-2023.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → 𝑋 ≠ 𝑌)
Theorem	velcomp 3966	Characterization of setvar elements of the complement of a class. (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴)
Theorem	elin 3967	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 3968*	Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30446). Note that 𝐴 ⊆ 𝐴 (proved in ssid 4006). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3971). For an alternative definition, not requiring a dummy variable, see dfss2 3969. Other possible definitions are given by dfss3 3972, dfss4 4269, sspss 4102, ssequn1 4186, ssequn2 4189, sseqin2 4223, and ssdif0 4366. 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 11163 and 1ex 11257) or ℝ ( cf. df-r 11165 and reex 11246). 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 11246). 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 3969. (Revised by GG, 15-May-2025.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
Theorem	dfss2 3969	Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3968. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3968. (Revised by GG, 15-May-2025.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
Theorem	dfss 3970	Variant of subclass definition dfss2 3969. (Contributed by NM, 21-Jun-1993.)
⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
Definition	df-pss 3971	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 30447). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4103). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3968). Other possible definitions are given by dfpss2 4088 and dfpss3 4089. (Contributed by NM, 7-Feb-1996.)
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
Theorem	dfss3 3972*	Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	dfss6 3973*	Alternate definition of subclass relationship. (Contributed by RP, 16-Apr-2020.)
⊢ (𝐴 ⊆ 𝐵 ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
Theorem	dfssf 3974	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 2377. (Revised by GG, 19-May-2023.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
Theorem	dfss3f 3975	Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	nfss 3976	If 𝑥 is not free in 𝐴 and 𝐵, it is not free in 𝐴 ⊆ 𝐵. (Contributed by NM, 27-Dec-1996.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵
Theorem	ssel 3977	Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) Avoid ax-12 2177. (Revised by SN, 27-May-2024.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
Theorem	ssel2 3978	Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)
Theorem	sseli 3979	Membership implication from subclass relationship. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
Theorem	sselii 3980	Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐶 ∈ 𝐴    ⇒   ⊢ 𝐶 ∈ 𝐵
Theorem	sselid 3981	Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐵)
Theorem	sseld 3982	Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
Theorem	sselda 3983	Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)
Theorem	sseldd 3984	Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐵)
Theorem	ssneld 3985	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 3986	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 3987*	Inference based on subclass definition. (Contributed by NM, 21-Jun-1993.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)    ⇒   ⊢ 𝐴 ⊆ 𝐵
Theorem	ssrd 3988	Deduction based on subclass definition. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	ssrdv 3989*	Deduction based on subclass definition. (Contributed by NM, 15-Nov-1995.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	sstr2 3990	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	sstr2OLD 3991	Obsolete version of sstr2 3990 as of 19-May-2025. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
Theorem	sstr 3992	Transitivity of subclass relationship. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)
Theorem	sstri 3993	Subclass transitivity inference. (Contributed by NM, 5-May-2000.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ 𝐴 ⊆ 𝐶
Theorem	sstrd 3994	Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sstrid 3995	Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sstrdi 3996	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	sylan9ss 3997	A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜓 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶)
Theorem	sylan9ssr 3998	A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜓 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝐴 ⊆ 𝐶)
Theorem	eqss 3999	The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 21-May-1993.)
⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
Theorem	eqssi 4000	Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐵 ⊆ 𝐴    ⇒   ⊢ 𝐴 = 𝐵