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	rspsbc 3901*	Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. This provides an axiom for a predicate calculus for a restricted domain. This theorem generalizes the unrestricted stdpc4 2068 and spsbc 3817. See also rspsbca 3902 and rspcsbela 4461. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → [𝐴 / 𝑥]𝜑))
Theorem	rspsbca 3902*	Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. (Contributed by NM, 14-Dec-2005.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → [𝐴 / 𝑥]𝜑)
Theorem	rspesbca 3903*	Existence form of rspsbca 3902. (Contributed by NM, 29-Feb-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ ((𝐴 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	spesbc 3904	Existence form of spsbc 3817. (Contributed by Mario Carneiro, 18-Nov-2016.)
⊢ ([𝐴 / 𝑥]𝜑 → ∃𝑥𝜑)
Theorem	spesbcd 3905	form of spsbc 3817. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ (𝜑 → [𝐴 / 𝑥]𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	sbcth2 3906*	A substitution into a theorem. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ (𝑥 ∈ 𝐵 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝐵 → [𝐴 / 𝑥]𝜑)
Theorem	ra4v 3907*	Version of ra4 3908 with a disjoint variable condition, requiring fewer axioms. This is stdpc5v 1937 for a restricted domain. (Contributed by BJ, 27-Mar-2020.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	ra4 3908	Restricted quantifier version of Axiom 5 of [Mendelson] p. 69. This is the axiom stdpc5 2209 of standard predicate calculus for a restricted domain. See ra4v 3907 for a version requiring fewer axioms. (Contributed by NM, 16-Jan-2004.) (Proof shortened by BJ, 27-Mar-2020.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	rmo2 3909*	Alternate definition of restricted "at most one". Note that ∃*𝑥 ∈ 𝐴𝜑 is not equivalent to ∃𝑦 ∈ 𝐴∀𝑥 ∈ 𝐴(𝜑 → 𝑥 = 𝑦) (in analogy to reu6 3748); to see this, let 𝐴 be the empty set. However, one direction of this pattern holds; see rmo2i 3910. (Contributed by NM, 17-Jun-2017.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))
Theorem	rmo2i 3910*	Condition implying restricted "at most one". (Contributed by NM, 17-Jun-2017.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	rmo3 3911*	Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) Avoid ax-13 2380. (Revised by Wolf Lammen, 30-Apr-2023.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
Theorem	rmob 3912*	Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((∃*𝑥 ∈ 𝐴 𝜑 ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒)))
Theorem	rmoi 3913*	Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((∃*𝑥 ∈ 𝐴 𝜑 ∧ (𝐵 ∈ 𝐴 ∧ 𝜓) ∧ (𝐶 ∈ 𝐴 ∧ 𝜒)) → 𝐵 = 𝐶)
Theorem	rmob2 3914*	Consequence of "restricted at most one". (Contributed by Thierry Arnoux, 9-Dec-2019.)
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝑥 = 𝐵 ↔ 𝜒))
Theorem	rmoi2 3915*	Consequence of "restricted at most one". (Contributed by Thierry Arnoux, 9-Dec-2019.)
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → 𝑥 = 𝐵)
Theorem	rmoanim 3916	Introduction of a conjunct into restricted "at most one" quantifier, analogous to moanim 2623. (Contributed by Alexander van der Vekens, 25-Jun-2017.) Avoid ax-10 2141 and ax-11 2158. (Revised by GG, 24-Aug-2023.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓))
Theorem	rmoanimALT 3917	Alternate proof of rmoanim 3916, shorter but requiring ax-10 2141 and ax-11 2158. (Contributed by Alexander van der Vekens, 25-Jun-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓))
Theorem	reuan 3918	Introduction of a conjunct into restricted unique existential quantifier, analogous to euan 2624. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓))
Theorem	2reu1 3919*	Double restricted existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one, analogous to 2eu1 2654. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
⊢ (∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)))
Theorem	2reu2 3920*	Double restricted existential uniqueness, analogous to 2eu2 2656. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
⊢ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
2.1.10  Proper substitution of classes for sets into classes
Syntax	csb 3921	Extend class notation to include the proper substitution of a class for a set into another class.
class ⦋𝐴 / 𝑥⦌𝐵
Definition	df-csb 3922*	Define the proper substitution of a class for a set into another class. The underlined brackets distinguish it from the substitution into a wff, wsbc 3804, to prevent ambiguity. Theorem sbcel1g 4439 shows an example of how ambiguity could arise if we did not use distinguished brackets. When 𝐴 is a proper class, this evaluates to the empty set (see csbprc 4432). Theorem sbccsb 4459 recovers substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)
⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
Theorem	csb2 3923*	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 3924	Analogue of dfsbcq 3806 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)
Theorem	csbeq1d 3925	Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)
Theorem	csbeq2 3926	Substituting into equivalent classes gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
⊢ (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2d 3927	Formula-building deduction for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2dv 3928*	Formula-building deduction for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2i 3929	Formula-building inference for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶
Theorem	csbeq12dv 3930*	Formula-building inference for class substitution. (Contributed by SN, 3-Nov-2023.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐷)
Theorem	cbvcsbw 3931*	Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on 𝐴. Version of cbvcsb 3932 with a disjoint variable condition, which does not require ax-13 2380. (Contributed by Jeff Hankins, 13-Sep-2009.) Avoid ax-13 2380. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑦⦌𝐷
Theorem	cbvcsb 3932	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 2380. Use the weaker cbvcsbw 3931 when possible. (Contributed by Jeff Hankins, 13-Sep-2009.) (Revised by Mario Carneiro, 11-Dec-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑦⦌𝐷
Theorem	cbvcsbv 3933*	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 3934	Analogue of sbid 2256 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴
Theorem	csbeq1a 3935	Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
Theorem	csbcow 3936*	Composition law for chained substitutions into a class. Version of csbco 3937 with a disjoint variable condition, which does not require ax-13 2380. (Contributed by NM, 10-Nov-2005.) Avoid ax-13 2380. (Revised by GG, 10-Jan-2024.)
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵
Theorem	csbco 3937*	Composition law for chained substitutions into a class. Usage of this theorem is discouraged because it depends on ax-13 2380. Use the weaker csbcow 3936 when possible. (Contributed by NM, 10-Nov-2005.) (New usage is discouraged.)
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵
Theorem	csbtt 3938	Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐵) → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)
Theorem	csbconstgf 3939	Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by NM, 10-Nov-2005.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)
Theorem	csbconstg 3940*	Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3939 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2178. (Revised by GG, 15-Oct-2024.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)
Theorem	csbconstgOLD 3941*	Obsolete version of csbconstg 3940 as of 15-Oct-2024. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)
Theorem	csbgfi 3942	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 3943*	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 3944	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵)
Theorem	nfcsb1 3945	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵
Theorem	nfcsb1v 3946*	Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵
Theorem	nfcsbd 3947	Deduction version of nfcsb 3949. Usage of this theorem is discouraged because it depends on ax-13 2380. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵)
Theorem	nfcsbw 3948*	Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3949 with a disjoint variable condition, which does not require ax-13 2380. (Contributed by Mario Carneiro, 12-Oct-2016.) Avoid ax-13 2380. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵
Theorem	nfcsb 3949	Bound-variable hypothesis builder for substitution into a class. Usage of this theorem is discouraged because it depends on ax-13 2380. Use the weaker nfcsbw 3948 when possible. (Contributed by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵
Theorem	csbhypf 3950*	Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 3556 for class substitution version. (Contributed by NM, 19-Dec-2008.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbiebt 3951*	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3955.) (Contributed by NM, 11-Nov-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶))
Theorem	csbiedf 3952*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbieb 3953*	Bidirectional conversion between an implicit class substitution hypothesis 𝑥 = 𝐴 → 𝐵 = 𝐶 and its explicit substitution equivalent. (Contributed by NM, 2-Mar-2008.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbiebg 3954*	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 3955*	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 3956*	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 3957*	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	csbieOLD 3958*	Obsolete version of csbie 3957 as of 15-Oct-2024. (Contributed by AV, 2-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶
Theorem	csbied 3959*	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	csbiedOLD 3960*	Obsolete version of csbied 3959 as of 15-Oct-2024. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbied2 3961*	Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷)
Theorem	csbie2t 3962*	Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 3963). (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷)
Theorem	csbie2 3963*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷
Theorem	csbie2g 3964*	Conversion of implicit substitution to explicit class substitution. This version of csbie 3957 avoids a disjointness condition on 𝑥, 𝐴 and 𝑥, 𝐷 by substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    &   ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷)
Theorem	cbvrabcsfw 3965*	Version of cbvrabcsf 3969 with a disjoint variable condition, which does not require ax-13 2380. (Contributed by Andrew Salmon, 13-Jul-2011.) (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓}
Theorem	cbvralcsf 3966	A more general version of cbvralf 3368 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 2380. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrexcsf 3967	A more general version of cbvrexf 3369 that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2380. (Contributed by Andrew Salmon, 13-Jul-2011.) (Proof shortened by Mario Carneiro, 7-Dec-2014.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
Theorem	cbvreucsf 3968	A more general version of cbvreuv 3438 that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2380. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrabcsf 3969	A more general version of cbvrab 3487 with no distinct variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2380. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓}
Theorem	cbvralv2 3970*	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 2380. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)
Theorem	cbvrexv2 3971*	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 2380. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)
Theorem	rspc2vd 3972*	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 3973	Extend class notation to include class difference (read: "𝐴 minus 𝐵").
class (𝐴 ∖ 𝐵)
Syntax	cun 3974	Extend class notation to include union of two classes (read: "𝐴 union 𝐵").
class (𝐴 ∪ 𝐵)
Syntax	cin 3975	Extend class notation to include the intersection of two classes (read: "𝐴 intersect 𝐵").
class (𝐴 ∩ 𝐵)
Syntax	wss 3976	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 3977	Extend wff notation with proper subclass relation.
wff 𝐴 ⊊ 𝐵
Theorem	difjust 3978*	Soundness justification theorem for df-dif 3979. (Contributed by Rodolfo Medina, 27-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)}
Definition	df-dif 3979*	Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. For example, ({1, 3} ∖ {1, 8}) = {3} (ex-dif 30455). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3981) and intersection (𝐴 ∩ 𝐵) (df-in 3983). 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 3980*	Soundness justification theorem for df-un 3981. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)}
Definition	df-un 3981*	Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∪ {1, 8}) = {1, 3, 8} (ex-un 30456). Contrast this operation with difference (𝐴 ∖ 𝐵) (df-dif 3979) and intersection (𝐴 ∩ 𝐵) (df-in 3983). For an alternate definition in terms of class difference, requiring no dummy variables, see dfun2 4289. For union defined in terms of intersection, see dfun3 4295. (Contributed by NM, 23-Aug-1993.)
⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)}
Theorem	injust 3982*	Soundness justification theorem for df-in 3983. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
Definition	df-in 3983*	Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 30457). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3981) and difference (𝐴 ∖ 𝐵) (df-dif 3979). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4290 and dfin4 4297. For intersection defined in terms of union, see dfin3 4296. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
Theorem	dfin5 3984*	Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.)
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}
Theorem	dfdif2 3985*	Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.)
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵}
Theorem	eldif 3986	Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
Theorem	eldifd 3987	If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3986. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))
Theorem	eldifad 3988	If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3986. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐵)
Theorem	eldifbd 3989	If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3986. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)
Theorem	elneeldif 3990	The elements of a set difference and the minuend are not equal. (Contributed by AV, 21-Oct-2023.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → 𝑋 ≠ 𝑌)
Theorem	velcomp 3991	Characterization of setvar elements of the complement of a class. (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴)
Theorem	elin 3992	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 3993*	Define the subclass relationship. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 30459). Note that 𝐴 ⊆ 𝐴 (proved in ssid 4031). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3996). For an alternative definition, not requiring a dummy variable, see dfss2 3994. Other possible definitions are given by dfss3 3997, dfss4 4288, sspss 4125, ssequn1 4209, ssequn2 4212, sseqin2 4244, and ssdif0 4389. 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 11192 and 1ex 11286) or ℝ ( cf. df-r 11194 and reex 11275). 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 11275). 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 3994. (Revised by GG, 15-May-2025.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
Theorem	dfss2 3994	Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3993. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3993. (Revised by GG, 15-May-2025.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
Theorem	dfss 3995	Variant of subclass definition dfss2 3994. (Contributed by NM, 21-Jun-1993.)
⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
Definition	df-pss 3996	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 30460). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4126). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3993). Other possible definitions are given by dfpss2 4111 and dfpss3 4112. (Contributed by NM, 7-Feb-1996.)
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
Theorem	dfss3 3997*	Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	dfss6 3998*	Alternate definition of subclass relationship. (Contributed by RP, 16-Apr-2020.)
⊢ (𝐴 ⊆ 𝐵 ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
Theorem	dfssf 3999	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 2380. (Revised by GG, 19-May-2023.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
Theorem	dfss3f 4000	Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)