P. 39 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 3801-3900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sbcg 3801*	Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3799. (Contributed by Alan Sare, 10-Nov-2012.) Reduce axiom usage. (Revised by GG, 12-Oct-2024.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑))
Theorem	sbcgfi 3802	Substitution for a variable not free in a wff does not affect it, in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜑)
Theorem	sbc2iegf 3803*	Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ Ⅎ𝑥 𝐵 ∈ 𝑊    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ 𝜓))
Theorem	sbc2ie 3804*	Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008.) (Revised by Mario Carneiro, 19-Dec-2013.) (Proof shortened by GG, 12-Oct-2024.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ 𝜓)
Theorem	sbc2iedv 3805*	Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008.) (Proof shortened by Mario Carneiro, 18-Oct-2016.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜓 ↔ 𝜒))
Theorem	sbc3ie 3806*	Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Jun-2014.) (Revised by Mario Carneiro, 29-Dec-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦][𝐶 / 𝑧]𝜑 ↔ 𝜓)
Theorem	sbccomlem 3807*	Lemma for sbccom 3809. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 18-Oct-2016.) Avoid ax-10 2147, ax-12 2185. (Revised by SN, 20-Aug-2025.)
⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccomlemOLD 3808*	Obsolete version of sbccomlem 3807 as of 20-Aug-2025. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 18-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom 3809*	Commutative law for double class substitution. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Mario Carneiro, 18-Oct-2016.)
⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbcralt 3810*	Interchange class substitution and restricted quantifier. (Contributed by NM, 1-Mar-2008.) (Revised by David Abernethy, 22-Feb-2010.)
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑))
Theorem	sbcrext 3811*	Interchange class substitution and restricted existential quantifier. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.) (Revised by NM, 18-Aug-2018.) (Proof shortened by JJ, 7-Jul-2021.)
⊢ (Ⅎ𝑦𝐴 → ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑))
Theorem	sbcralg 3812*	Interchange class substitution and restricted quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑))
Theorem	sbcrex 3813*	Interchange class substitution and restricted existential quantifier. (Contributed by NM, 15-Nov-2005.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)
Theorem	sbcreu 3814*	Interchange class substitution and restricted unique existential quantifier. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)
Theorem	reu8nf 3815*	Restricted uniqueness using implicit substitution. This version of reu8 3679 uses a nonfreeness hypothesis for 𝑥 and 𝜓 instead of distinct variable conditions. (Contributed by AV, 21-Jan-2022.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑤 = 𝑦 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))
Theorem	sbcabel 3816*	Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]{𝑦 ∣ 𝜑} ∈ 𝐵 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝜑} ∈ 𝐵))
Theorem	rspsbc 3817*	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 2074 and spsbc 3741. See also rspsbca 3818 and rspcsbela 4378. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → [𝐴 / 𝑥]𝜑))
Theorem	rspsbca 3818*	Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. (Contributed by NM, 14-Dec-2005.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → [𝐴 / 𝑥]𝜑)
Theorem	rspesbca 3819*	Existence form of rspsbca 3818. (Contributed by NM, 29-Feb-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ ((𝐴 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	spesbc 3820	Existence form of spsbc 3741. (Contributed by Mario Carneiro, 18-Nov-2016.)
⊢ ([𝐴 / 𝑥]𝜑 → ∃𝑥𝜑)
Theorem	spesbcd 3821	form of spsbc 3741. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ (𝜑 → [𝐴 / 𝑥]𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	sbcth2 3822*	A substitution into a theorem. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ (𝑥 ∈ 𝐵 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝐵 → [𝐴 / 𝑥]𝜑)
Theorem	ra4v 3823*	Version of ra4 3824 with a disjoint variable condition, requiring fewer axioms. This is stdpc5v 1940 for a restricted domain. (Contributed by BJ, 27-Mar-2020.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	ra4 3824	Restricted quantifier version of Axiom 5 of [Mendelson] p. 69. This is the axiom stdpc5 2216 of standard predicate calculus for a restricted domain. See ra4v 3823 for a version requiring fewer axioms. (Contributed by NM, 16-Jan-2004.) (Proof shortened by BJ, 27-Mar-2020.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	rmo2 3825*	Alternate definition of restricted "at most one". Note that ∃*𝑥 ∈ 𝐴𝜑 is not equivalent to ∃𝑦 ∈ 𝐴∀𝑥 ∈ 𝐴(𝜑 → 𝑥 = 𝑦) (in analogy to reu6 3672); to see this, let 𝐴 be the empty set. However, one direction of this pattern holds; see rmo2i 3826. (Contributed by NM, 17-Jun-2017.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))
Theorem	rmo2i 3826*	Condition implying restricted "at most one". (Contributed by NM, 17-Jun-2017.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	rmo3 3827*	Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) Avoid ax-13 2376. (Revised by Wolf Lammen, 30-Apr-2023.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
Theorem	rmob 3828*	Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((∃*𝑥 ∈ 𝐴 𝜑 ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒)))
Theorem	rmoi 3829*	Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((∃*𝑥 ∈ 𝐴 𝜑 ∧ (𝐵 ∈ 𝐴 ∧ 𝜓) ∧ (𝐶 ∈ 𝐴 ∧ 𝜒)) → 𝐵 = 𝐶)
Theorem	rmob2 3830*	Consequence of "restricted at most one". (Contributed by Thierry Arnoux, 9-Dec-2019.)
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝑥 = 𝐵 ↔ 𝜒))
Theorem	rmoi2 3831*	Consequence of "restricted at most one". (Contributed by Thierry Arnoux, 9-Dec-2019.)
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → 𝑥 = 𝐵)
Theorem	rmoanim 3832	Introduction of a conjunct into restricted "at most one" quantifier, analogous to moanim 2620. (Contributed by Alexander van der Vekens, 25-Jun-2017.) Avoid ax-10 2147 and ax-11 2163. (Revised by GG, 24-Aug-2023.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓))
Theorem	rmoanimALT 3833	Alternate proof of rmoanim 3832, shorter but requiring ax-10 2147 and ax-11 2163. (Contributed by Alexander van der Vekens, 25-Jun-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓))
Theorem	reuan 3834	Introduction of a conjunct into restricted unique existential quantifier, analogous to euan 2621. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓))
Theorem	2reu1 3835*	Double restricted existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one, analogous to 2eu1 2651. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
⊢ (∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)))
Theorem	2reu2 3836*	Double restricted existential uniqueness, analogous to 2eu2 2653. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
⊢ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
2.1.10  Proper substitution of classes for sets into classes
Syntax	csb 3837	Extend class notation to include the proper substitution of a class for a set into another class.
class ⦋𝐴 / 𝑥⦌𝐵
Definition	df-csb 3838*	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 3728, to prevent ambiguity. Theorem sbcel1g 4356 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 4349). Theorem sbccsb 4376 recovers substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)
⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
Theorem	csb2 3839*	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 3840	Analogue of dfsbcq 3730 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)
Theorem	csbeq1d 3841	Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)
Theorem	csbeq2 3842	Substituting into equivalent classes gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
⊢ (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2d 3843	Formula-building deduction for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2dv 3844*	Formula-building deduction for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2i 3845	Formula-building inference for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶
Theorem	csbeq12dv 3846*	Formula-building inference for class substitution. (Contributed by SN, 3-Nov-2023.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐷)
Theorem	cbvcsbw 3847*	Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on 𝐴. Version of cbvcsb 3848 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by Jeff Hankins, 13-Sep-2009.) Avoid ax-13 2376. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑦⦌𝐷
Theorem	cbvcsb 3848	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 2376. Use the weaker cbvcsbw 3847 when possible. (Contributed by Jeff Hankins, 13-Sep-2009.) (Revised by Mario Carneiro, 11-Dec-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑦⦌𝐷
Theorem	cbvcsbv 3849*	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 3850	Analogue of sbid 2263 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴
Theorem	csbeq1a 3851	Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
Theorem	csbcow 3852*	Composition law for chained substitutions into a class. Version of csbco 3853 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by NM, 10-Nov-2005.) Avoid ax-13 2376. (Revised by GG, 10-Jan-2024.)
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵
Theorem	csbco 3853*	Composition law for chained substitutions into a class. Usage of this theorem is discouraged because it depends on ax-13 2376. Use the weaker csbcow 3852 when possible. (Contributed by NM, 10-Nov-2005.) (New usage is discouraged.)
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵
Theorem	csbtt 3854	Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐵) → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)
Theorem	csbconstgf 3855	Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by NM, 10-Nov-2005.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)
Theorem	csbconstg 3856*	Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3855 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2185. (Revised by GG, 15-Oct-2024.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)
Theorem	csbgfi 3857	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 3858*	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 3859	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵)
Theorem	nfcsb1 3860	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵
Theorem	nfcsb1v 3861*	Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵
Theorem	nfcsbd 3862	Deduction version of nfcsb 3864. Usage of this theorem is discouraged because it depends on ax-13 2376. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵)
Theorem	nfcsbw 3863*	Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3864 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by Mario Carneiro, 12-Oct-2016.) Avoid ax-13 2376. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵
Theorem	nfcsb 3864	Bound-variable hypothesis builder for substitution into a class. Usage of this theorem is discouraged because it depends on ax-13 2376. Use the weaker nfcsbw 3863 when possible. (Contributed by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵
Theorem	csbhypf 3865*	Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 3490 for class substitution version. (Contributed by NM, 19-Dec-2008.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbiebt 3866*	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3870.) (Contributed by NM, 11-Nov-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶))
Theorem	csbiedf 3867*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbieb 3868*	Bidirectional conversion between an implicit class substitution hypothesis 𝑥 = 𝐴 → 𝐵 = 𝐶 and its explicit substitution equivalent. (Contributed by NM, 2-Mar-2008.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbiebg 3869*	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 3870*	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 3871*	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 3872*	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 3873*	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 3874*	Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷)
Theorem	csbie2t 3875*	Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 3876). (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷)
Theorem	csbie2 3876*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷
Theorem	csbie2g 3877*	Conversion of implicit substitution to explicit class substitution. This version of csbie 3872 avoids a disjointness condition on 𝑥, 𝐴 and 𝑥, 𝐷 by substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    &   ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷)
Theorem	cbvrabcsfw 3878*	Version of cbvrabcsf 3882 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by Andrew Salmon, 13-Jul-2011.) (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓}
Theorem	cbvralcsf 3879	A more general version of cbvralf 3322 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 2376. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrexcsf 3880	A more general version of cbvrexf 3323 that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2376. (Contributed by Andrew Salmon, 13-Jul-2011.) (Proof shortened by Mario Carneiro, 7-Dec-2014.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
Theorem	cbvreucsf 3881	A more general version of cbvreuv 3384 that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2376. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrabcsf 3882	A more general version of cbvrab 3428 with no distinct variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2376. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓}
Theorem	cbvralv2 3883*	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 2376. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)
Theorem	cbvrexv2 3884*	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 2376. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)
Theorem	rspc2vd 3885*	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 3886	Extend class notation to include class difference (read: "𝐴 minus 𝐵").
class (𝐴 ∖ 𝐵)
Syntax	cun 3887	Extend class notation to include union of two classes (read: "𝐴 union 𝐵").
class (𝐴 ∪ 𝐵)
Syntax	cin 3888	Extend class notation to include the intersection of two classes (read: "𝐴 intersect 𝐵").
class (𝐴 ∩ 𝐵)
Syntax	wss 3889	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 3890	Extend wff notation with proper subclass relation.
wff 𝐴 ⊊ 𝐵
Theorem	difjust 3891*	Soundness justification theorem for df-dif 3892. (Contributed by Rodolfo Medina, 27-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)}
Definition	df-dif 3892*	Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. For example, ({1, 3} ∖ {1, 8}) = {3} (ex-dif 30493). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3894) and intersection (𝐴 ∩ 𝐵) (df-in 3896). 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 3893*	Soundness justification theorem for df-un 3894. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)}
Definition	df-un 3894*	Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∪ {1, 8}) = {1, 3, 8} (ex-un 30494). Contrast this operation with difference (𝐴 ∖ 𝐵) (df-dif 3892) and intersection (𝐴 ∩ 𝐵) (df-in 3896). For an alternate definition in terms of class difference, requiring no dummy variables, see dfun2 4210. For union defined in terms of intersection, see dfun3 4216. (Contributed by NM, 23-Aug-1993.)
⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)}
Theorem	injust 3895*	Soundness justification theorem for df-in 3896. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
Definition	df-in 3896*	Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 30495). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3894) and difference (𝐴 ∖ 𝐵) (df-dif 3892). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4211 and dfin4 4218. For intersection defined in terms of union, see dfin3 4217. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
Theorem	dfin5 3897*	Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.)
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}
Theorem	dfdif2 3898*	Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.)
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵}
Theorem	eldif 3899	Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
Theorem	eldifd 3900	If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3899. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))