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	sbcng 3801	Move negation in and out of class substitution. (Contributed by NM, 16-Jan-2004.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ [𝐴 / 𝑥]𝜑))
Theorem	sbcimg 3802	Distribution of class substitution over implication. (Contributed by NM, 16-Jan-2004.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)))
Theorem	sbcan 3803	Distribution of class substitution over conjunction. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 17-Aug-2018.)
⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓))
Theorem	sbcor 3804	Distribution of class substitution over disjunction. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 17-Aug-2018.)
⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓))
Theorem	sbcbig 3805	Distribution of class substitution over biconditional. (Contributed by Raph Levien, 10-Apr-2004.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)))
Theorem	sbcn1 3806	Move negation in and out of class substitution. One direction of sbcng 3801 that holds for proper classes. (Contributed by NM, 17-Aug-2018.)
⊢ ([𝐴 / 𝑥] ¬ 𝜑 → ¬ [𝐴 / 𝑥]𝜑)
Theorem	sbcim1 3807	Distribution of class substitution over implication. One direction of sbcimg 3802 that holds for proper classes. (Contributed by NM, 17-Aug-2018.) Avoid ax-10 2142, ax-12 2178. (Revised by SN, 26-Oct-2024.)
⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓))
Theorem	sbcbid 3808	Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒))
Theorem	sbcbidv 3809*	Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014.) Drop ax-12 2178. (Revised by GG, 1-Dec-2023.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒))
Theorem	sbcbii 3810	Formula-building inference for class substitution. (Contributed by NM, 11-Nov-2005.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)
Theorem	sbcbi1 3811	Distribution of class substitution over biconditional. One direction of sbcbig 3805 that holds for proper classes. (Contributed by NM, 17-Aug-2018.)
⊢ ([𝐴 / 𝑥](𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))
Theorem	sbcbi2 3812	Substituting into equivalent wff's gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.) (Proof shortened by Wolf Lammen, 4-May-2023.) Avoid ax-10 2142, ax-12 2178. (Revised by Steven Nguyen, 5-May-2024.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))
Theorem	sbcal 3813*	Move universal quantifier in and out of class substitution. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝐴 / 𝑦]𝜑)
Theorem	sbcex2 3814*	Move existential quantifier in and out of class substitution. (Contributed by NM, 21-May-2004.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑)
Theorem	sbceqal 3815*	Class version of one implication of equvelv 2031. (Contributed by Andrew Salmon, 28-Jun-2011.) (Proof shortened by SN, 26-Oct-2024.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝑥 = 𝐵) → 𝐴 = 𝐵))
Theorem	sbeqalb 3816*	Theorem *14.121 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 28-Jun-2011.) (Proof shortened by Wolf Lammen, 9-May-2013.)
⊢ (𝐴 ∈ 𝑉 → ((∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ∧ ∀𝑥(𝜑 ↔ 𝑥 = 𝐵)) → 𝐴 = 𝐵))
Theorem	eqsbc2 3817*	Substitution for the right-hand side in an equality. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by JJ, 7-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝑥 ↔ 𝐵 = 𝐴))
Theorem	sbc3an 3818	Distribution of class substitution over triple conjunction. (Contributed by NM, 14-Dec-2006.) (Revised by NM, 17-Aug-2018.)
⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓 ∧ [𝐴 / 𝑥]𝜒))
Theorem	sbcel1v 3819*	Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.) Avoid ax-13 2370. (Revised by Wolf Lammen, 30-Apr-2023.)
⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)
Theorem	sbcel2gv 3820*	Class substitution into a membership relation. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (𝐵 ∈ 𝑉 → ([𝐵 / 𝑥]𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
Theorem	sbcel21v 3821*	Class substitution into a membership relation. One direction of sbcel2gv 3820 that holds for proper classes. (Contributed by NM, 17-Aug-2018.)
⊢ ([𝐵 / 𝑥]𝐴 ∈ 𝑥 → 𝐴 ∈ 𝐵)
Theorem	sbcimdv 3822*	Substitution analogue of Theorem 19.20 of [Margaris] p. 90 (alim 1810). (Contributed by NM, 11-Nov-2005.) (Revised by NM, 17-Aug-2018.) (Proof shortened by JJ, 7-Jul-2021.) Reduce axiom usage. (Revised by GG, 12-Oct-2024.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))
Theorem	sbctt 3823	Substitution for a variable not free in a wff does not affect it. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝜑) → ([𝐴 / 𝑥]𝜑 ↔ 𝜑))
Theorem	sbcgf 3824	Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 11-Oct-2004.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑))
Theorem	sbc19.21g 3825	Substitution for a variable not free in antecedent affects only the consequent. (Contributed by NM, 11-Oct-2004.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝐴 / 𝑥]𝜓)))
Theorem	sbcg 3826*	Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3824. (Contributed by Alan Sare, 10-Nov-2012.) Reduce axiom usage. (Revised by GG, 12-Oct-2024.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑))
Theorem	sbcgfi 3827	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 3828*	Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ Ⅎ𝑥 𝐵 ∈ 𝑊    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ 𝜓))
Theorem	sbc2ie 3829*	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 3830*	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 3831*	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 3832*	Lemma for sbccom 3834. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 18-Oct-2016.) Avoid ax-10 2142, ax-12 2178. (Revised by SN, 20-Aug-2025.)
⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccomlemOLD 3833*	Obsolete version of sbccomlem 3832 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 3834*	Commutative law for double class substitution. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Mario Carneiro, 18-Oct-2016.)
⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbcralt 3835*	Interchange class substitution and restricted quantifier. (Contributed by NM, 1-Mar-2008.) (Revised by David Abernethy, 22-Feb-2010.)
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑))
Theorem	sbcrext 3836*	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 3837*	Interchange class substitution and restricted quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑))
Theorem	sbcrex 3838*	Interchange class substitution and restricted existential quantifier. (Contributed by NM, 15-Nov-2005.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)
Theorem	sbcreu 3839*	Interchange class substitution and restricted unique existential quantifier. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)
Theorem	reu8nf 3840*	Restricted uniqueness using implicit substitution. This version of reu8 3704 uses a nonfreeness hypothesis for 𝑥 and 𝜓 instead of distinct variable conditions. (Contributed by AV, 21-Jan-2022.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑤 = 𝑦 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))
Theorem	sbcabel 3841*	Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]{𝑦 ∣ 𝜑} ∈ 𝐵 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝜑} ∈ 𝐵))
Theorem	rspsbc 3842*	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 2069 and spsbc 3766. See also rspsbca 3843 and rspcsbela 4401. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → [𝐴 / 𝑥]𝜑))
Theorem	rspsbca 3843*	Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. (Contributed by NM, 14-Dec-2005.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → [𝐴 / 𝑥]𝜑)
Theorem	rspesbca 3844*	Existence form of rspsbca 3843. (Contributed by NM, 29-Feb-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ ((𝐴 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	spesbc 3845	Existence form of spsbc 3766. (Contributed by Mario Carneiro, 18-Nov-2016.)
⊢ ([𝐴 / 𝑥]𝜑 → ∃𝑥𝜑)
Theorem	spesbcd 3846	form of spsbc 3766. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ (𝜑 → [𝐴 / 𝑥]𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	sbcth2 3847*	A substitution into a theorem. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ (𝑥 ∈ 𝐵 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝐵 → [𝐴 / 𝑥]𝜑)
Theorem	ra4v 3848*	Version of ra4 3849 with a disjoint variable condition, requiring fewer axioms. This is stdpc5v 1938 for a restricted domain. (Contributed by BJ, 27-Mar-2020.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	ra4 3849	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 3848 for a version requiring fewer axioms. (Contributed by NM, 16-Jan-2004.) (Proof shortened by BJ, 27-Mar-2020.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	rmo2 3850*	Alternate definition of restricted "at most one". Note that ∃*𝑥 ∈ 𝐴𝜑 is not equivalent to ∃𝑦 ∈ 𝐴∀𝑥 ∈ 𝐴(𝜑 → 𝑥 = 𝑦) (in analogy to reu6 3697); to see this, let 𝐴 be the empty set. However, one direction of this pattern holds; see rmo2i 3851. (Contributed by NM, 17-Jun-2017.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))
Theorem	rmo2i 3851*	Condition implying restricted "at most one". (Contributed by NM, 17-Jun-2017.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	rmo3 3852*	Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) Avoid ax-13 2370. (Revised by Wolf Lammen, 30-Apr-2023.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
Theorem	rmob 3853*	Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((∃*𝑥 ∈ 𝐴 𝜑 ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒)))
Theorem	rmoi 3854*	Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((∃*𝑥 ∈ 𝐴 𝜑 ∧ (𝐵 ∈ 𝐴 ∧ 𝜓) ∧ (𝐶 ∈ 𝐴 ∧ 𝜒)) → 𝐵 = 𝐶)
Theorem	rmob2 3855*	Consequence of "restricted at most one". (Contributed by Thierry Arnoux, 9-Dec-2019.)
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝑥 = 𝐵 ↔ 𝜒))
Theorem	rmoi2 3856*	Consequence of "restricted at most one". (Contributed by Thierry Arnoux, 9-Dec-2019.)
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → 𝑥 = 𝐵)
Theorem	rmoanim 3857	Introduction of a conjunct into restricted "at most one" quantifier, analogous to moanim 2613. (Contributed by Alexander van der Vekens, 25-Jun-2017.) Avoid ax-10 2142 and ax-11 2158. (Revised by GG, 24-Aug-2023.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓))
Theorem	rmoanimALT 3858	Alternate proof of rmoanim 3857, shorter but requiring ax-10 2142 and ax-11 2158. (Contributed by Alexander van der Vekens, 25-Jun-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓))
Theorem	reuan 3859	Introduction of a conjunct into restricted unique existential quantifier, analogous to euan 2614. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓))
Theorem	2reu1 3860*	Double restricted existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one, analogous to 2eu1 2644. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
⊢ (∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)))
Theorem	2reu2 3861*	Double restricted existential uniqueness, analogous to 2eu2 2646. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
⊢ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
2.1.10  Proper substitution of classes for sets into classes
Syntax	csb 3862	Extend class notation to include the proper substitution of a class for a set into another class.
class ⦋𝐴 / 𝑥⦌𝐵
Definition	df-csb 3863*	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 3753, to prevent ambiguity. Theorem sbcel1g 4379 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 4372). Theorem sbccsb 4399 recovers substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)
⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
Theorem	csb2 3864*	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 3865	Analogue of dfsbcq 3755 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)
Theorem	csbeq1d 3866	Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)
Theorem	csbeq2 3867	Substituting into equivalent classes gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
⊢ (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2d 3868	Formula-building deduction for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2dv 3869*	Formula-building deduction for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2i 3870	Formula-building inference for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶
Theorem	csbeq12dv 3871*	Formula-building inference for class substitution. (Contributed by SN, 3-Nov-2023.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐷)
Theorem	cbvcsbw 3872*	Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on 𝐴. Version of cbvcsb 3873 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by Jeff Hankins, 13-Sep-2009.) Avoid ax-13 2370. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑦⦌𝐷
Theorem	cbvcsb 3873	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 2370. Use the weaker cbvcsbw 3872 when possible. (Contributed by Jeff Hankins, 13-Sep-2009.) (Revised by Mario Carneiro, 11-Dec-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑦⦌𝐷
Theorem	cbvcsbv 3874*	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 3875	Analogue of sbid 2256 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴
Theorem	csbeq1a 3876	Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
Theorem	csbcow 3877*	Composition law for chained substitutions into a class. Version of csbco 3878 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by NM, 10-Nov-2005.) Avoid ax-13 2370. (Revised by GG, 10-Jan-2024.)
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵
Theorem	csbco 3878*	Composition law for chained substitutions into a class. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker csbcow 3877 when possible. (Contributed by NM, 10-Nov-2005.) (New usage is discouraged.)
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵
Theorem	csbtt 3879	Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐵) → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)
Theorem	csbconstgf 3880	Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by NM, 10-Nov-2005.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)
Theorem	csbconstg 3881*	Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3880 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2178. (Revised by GG, 15-Oct-2024.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)
Theorem	csbgfi 3882	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 3883*	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 3884	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵)
Theorem	nfcsb1 3885	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵
Theorem	nfcsb1v 3886*	Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵
Theorem	nfcsbd 3887	Deduction version of nfcsb 3889. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵)
Theorem	nfcsbw 3888*	Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3889 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by Mario Carneiro, 12-Oct-2016.) Avoid ax-13 2370. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵
Theorem	nfcsb 3889	Bound-variable hypothesis builder for substitution into a class. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker nfcsbw 3888 when possible. (Contributed by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵
Theorem	csbhypf 3890*	Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 3510 for class substitution version. (Contributed by NM, 19-Dec-2008.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbiebt 3891*	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3895.) (Contributed by NM, 11-Nov-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶))
Theorem	csbiedf 3892*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbieb 3893*	Bidirectional conversion between an implicit class substitution hypothesis 𝑥 = 𝐴 → 𝐵 = 𝐶 and its explicit substitution equivalent. (Contributed by NM, 2-Mar-2008.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)
Theorem	csbiebg 3894*	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 3895*	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 3896*	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 3897*	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 3898*	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 3899*	Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷)
Theorem	csbie2t 3900*	Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 3901). (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷)