P. 29 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2801-2900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sbcor 2801	Distribution of class substitution over disjunction. (Contributed by NM, 31-Dec-2016.)
⊢ ([A / x](φ ∨ ψ) ↔ ([A / x]φ ∨ [A / x]ψ))
Theorem	sbcorg 2802	Distribution of class substitution over disjunction. (Contributed by NM, 21-May-2004.)
⊢ (A ∈ 𝑉 → ([A / x](φ ∨ ψ) ↔ ([A / x]φ ∨ [A / x]ψ)))
Theorem	sbcbig 2803	Distribution of class substitution over biconditional. (Contributed by Raph Levien, 10-Apr-2004.)
⊢ (A ∈ 𝑉 → ([A / x](φ ↔ ψ) ↔ ([A / x]φ ↔ [A / x]ψ)))
Theorem	sbcal 2804*	Move universal quantifier in and out of class substitution. (Contributed by NM, 31-Dec-2016.)
⊢ ([A / y]∀xφ ↔ ∀x[A / y]φ)
Theorem	sbcalg 2805*	Move universal quantifier in and out of class substitution. (Contributed by NM, 16-Jan-2004.)
⊢ (A ∈ 𝑉 → ([A / y]∀xφ ↔ ∀x[A / y]φ))
Theorem	sbcex2 2806*	Move existential quantifier in and out of class substitution. (Contributed by NM, 21-May-2004.)
⊢ ([A / y]∃xφ ↔ ∃x[A / y]φ)
Theorem	sbcexg 2807*	Move existential quantifier in and out of class substitution. (Contributed by NM, 21-May-2004.)
⊢ (A ∈ 𝑉 → ([A / y]∃xφ ↔ ∃x[A / y]φ))
Theorem	sbceqal 2808*	A variation of extensionality for classes. (Contributed by Andrew Salmon, 28-Jun-2011.)
⊢ (A ∈ 𝑉 → (∀x(x = A → x = B) → A = B))
Theorem	sbeqalb 2809*	Theorem *14.121 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 28-Jun-2011.) (Proof shortened by Wolf Lammen, 9-May-2013.)
⊢ (A ∈ 𝑉 → ((∀x(φ ↔ x = A) ∧ ∀x(φ ↔ x = B)) → A = B))
Theorem	sbcbid 2810	Formula-building deduction rule for class substitution. (Contributed by NM, 29-Dec-2014.)
⊢ Ⅎxφ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ([A / x]ψ ↔ [A / x]χ))
Theorem	sbcbidv 2811*	Formula-building deduction rule for class substitution. (Contributed by NM, 29-Dec-2014.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ([A / x]ψ ↔ [A / x]χ))
Theorem	sbcbii 2812	Formula-building inference rule for class substitution. (Contributed by NM, 11-Nov-2005.)
⊢ (φ ↔ ψ)    ⇒   ⊢ ([A / x]φ ↔ [A / x]ψ)
Theorem	eqsbc3r 2813*	eqsbc3 2796 with setvar variable on right side of equals sign. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ (A ∈ B → ([A / x]𝐶 = x ↔ 𝐶 = A))
Theorem	sbc3ang 2814	Distribution of class substitution over triple conjunction. (Contributed by NM, 14-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (A ∈ 𝑉 → ([A / x](φ ∧ ψ ∧ χ) ↔ ([A / x]φ ∧ [A / x]ψ ∧ [A / x]χ)))
Theorem	sbcel1gv 2815*	Class substitution into a membership relation. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (A ∈ 𝑉 → ([A / x]x ∈ B ↔ A ∈ B))
Theorem	sbcel2gv 2816*	Class substitution into a membership relation. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (B ∈ 𝑉 → ([B / x]A ∈ x ↔ A ∈ B))
Theorem	sbcimdv 2817*	Substitution analog of Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 11-Nov-2005.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ ((φ ∧ A ∈ 𝑉) → ([A / x]ψ → [A / x]χ))
Theorem	sbctt 2818	Substitution for a variable not free in a wff does not affect it. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ ((A ∈ 𝑉 ∧ Ⅎxφ) → ([A / x]φ ↔ φ))
Theorem	sbcgf 2819	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.)
⊢ Ⅎxφ    ⇒   ⊢ (A ∈ 𝑉 → ([A / x]φ ↔ φ))
Theorem	sbc19.21g 2820	Substitution for a variable not free in antecedent affects only the consequent. (Contributed by NM, 11-Oct-2004.)
⊢ Ⅎxφ    ⇒   ⊢ (A ∈ 𝑉 → ([A / x](φ → ψ) ↔ (φ → [A / x]ψ)))
Theorem	sbcg 2821*	Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 2819. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (A ∈ 𝑉 → ([A / x]φ ↔ φ))
Theorem	sbc2iegf 2822*	Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ Ⅎxψ    &   ⊢ Ⅎyψ    &   ⊢ Ⅎx B ∈ 𝑊    &   ⊢ ((x = A ∧ y = B) → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → ([A / x][B / y]φ ↔ ψ))
Theorem	sbc2ie 2823*	Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ ((x = A ∧ y = B) → (φ ↔ ψ))    ⇒   ⊢ ([A / x][B / y]φ ↔ ψ)
Theorem	sbc2iedv 2824*	Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008.) (Proof shortened by Mario Carneiro, 18-Oct-2016.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (φ → ((x = A ∧ y = B) → (ψ ↔ χ)))    ⇒   ⊢ (φ → ([A / x][B / y]ψ ↔ χ))
Theorem	sbc3ie 2825*	Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Jun-2014.) (Revised by Mario Carneiro, 29-Dec-2014.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ ((x = A ∧ y = B ∧ z = 𝐶) → (φ ↔ ψ))    ⇒   ⊢ ([A / x][B / y][𝐶 / z]φ ↔ ψ)
Theorem	sbccomlem 2826*	Lemma for sbccom 2827. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 18-Oct-2016.)
⊢ ([A / x][B / y]φ ↔ [B / y][A / x]φ)
Theorem	sbccom 2827*	Commutative law for double class substitution. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Mario Carneiro, 18-Oct-2016.)
⊢ ([A / x][B / y]φ ↔ [B / y][A / x]φ)
Theorem	sbcralt 2828*	Interchange class substitution and restricted quantifier. (Contributed by NM, 1-Mar-2008.) (Revised by David Abernethy, 22-Feb-2010.)
⊢ ((A ∈ 𝑉 ∧ ℲyA) → ([A / x]∀y ∈ B φ ↔ ∀y ∈ B [A / x]φ))
Theorem	sbcrext 2829*	Interchange class substitution and restricted existential quantifier. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ ((A ∈ 𝑉 ∧ ℲyA) → ([A / x]∃y ∈ B φ ↔ ∃y ∈ B [A / x]φ))
Theorem	sbcralg 2830*	Interchange class substitution and restricted quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (A ∈ 𝑉 → ([A / x]∀y ∈ B φ ↔ ∀y ∈ B [A / x]φ))
Theorem	sbcrexg 2831*	Interchange class substitution and restricted existential quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (A ∈ 𝑉 → ([A / x]∃y ∈ B φ ↔ ∃y ∈ B [A / x]φ))
Theorem	sbcreug 2832*	Interchange class substitution and restricted uniqueness quantifier. (Contributed by NM, 24-Feb-2013.)
⊢ (A ∈ 𝑉 → ([A / x]∃!y ∈ B φ ↔ ∃!y ∈ B [A / x]φ))
Theorem	sbcabel 2833*	Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005.)
⊢ ℲxB    ⇒   ⊢ (A ∈ 𝑉 → ([A / x]{y ∣ φ} ∈ B ↔ {y ∣ [A / x]φ} ∈ B))
Theorem	rspsbc 2834*	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 1655 and spsbc 2769. See also rspsbca 2835 and rspcsbela . (Contributed by NM, 17-Nov-2006.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ (A ∈ B → (∀x ∈ B φ → [A / x]φ))
Theorem	rspsbca 2835*	Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. (Contributed by NM, 14-Dec-2005.)
⊢ ((A ∈ B ∧ ∀x ∈ B φ) → [A / x]φ)
Theorem	rspesbca 2836*	Existence form of rspsbca 2835. (Contributed by NM, 29-Feb-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ ((A ∈ B ∧ [A / x]φ) → ∃x ∈ B φ)
Theorem	spesbc 2837	Existence form of spsbc 2769. (Contributed by Mario Carneiro, 18-Nov-2016.)
⊢ ([A / x]φ → ∃xφ)
Theorem	spesbcd 2838	form of spsbc 2769. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ (φ → [A / x]ψ)    ⇒   ⊢ (φ → ∃xψ)
Theorem	sbcth2 2839*	A substitution into a theorem. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ (x ∈ B → φ)    ⇒   ⊢ (A ∈ B → [A / x]φ)
Theorem	ra5 2840	Restricted quantifier version of Axiom 5 of [Mendelson] p. 69. This is an axiom of a predicate calculus for a restricted domain. Compare the unrestricted stdpc5 1473. (Contributed by NM, 16-Jan-2004.)
⊢ Ⅎxφ    ⇒   ⊢ (∀x ∈ A (φ → ψ) → (φ → ∀x ∈ A ψ))
Theorem	rmo2ilem 2841*	Condition implying restricted "at most one." (Contributed by Jim Kingdon, 14-Jul-2018.)
⊢ Ⅎyφ    ⇒   ⊢ (∃y∀x ∈ A (φ → x = y) → ∃*x ∈ A φ)
Theorem	rmo2i 2842*	Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017.)
⊢ Ⅎyφ    ⇒   ⊢ (∃y ∈ A ∀x ∈ A (φ → x = y) → ∃*x ∈ A φ)
Theorem	rmo3 2843*	Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
⊢ Ⅎyφ    ⇒   ⊢ (∃*x ∈ A φ ↔ ∀x ∈ A ∀y ∈ A ((φ ∧ [y / x]φ) → x = y))
Theorem	rmob 2844*	Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.)
⊢ (x = B → (φ ↔ ψ))    &   ⊢ (x = 𝐶 → (φ ↔ χ))    ⇒   ⊢ ((∃*x ∈ A φ ∧ (B ∈ A ∧ ψ)) → (B = 𝐶 ↔ (𝐶 ∈ A ∧ χ)))
Theorem	rmoi 2845*	Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
⊢ (x = B → (φ ↔ ψ))    &   ⊢ (x = 𝐶 → (φ ↔ χ))    ⇒   ⊢ ((∃*x ∈ A φ ∧ (B ∈ A ∧ ψ) ∧ (𝐶 ∈ A ∧ χ)) → B = 𝐶)
2.1.10  Proper substitution of classes for sets into classes
Syntax	csb 2846	Extend class notation to include the proper substitution of a class for a set into another class.
class ⦋A / x⦌B
Definition	df-csb 2847*	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 2758, to prevent ambiguity. Theorem sbcel1g 2863 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2872 recreates substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)
⊢ ⦋A / x⦌B = {y ∣ [A / x]y ∈ B}
Theorem	csb2 2848*	Alternate expression for the proper substitution into a class, without referencing substitution into a wff. Note that x can be free in B but cannot occur in A. (Contributed by NM, 2-Dec-2013.)
⊢ ⦋A / x⦌B = {y ∣ ∃x(x = A ∧ y ∈ B)}
Theorem	csbeq1 2849	Analog of dfsbcq 2760 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (A = B → ⦋A / x⦌𝐶 = ⦋B / x⦌𝐶)
Theorem	cbvcsb 2850	Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on A. (Contributed by Jeff Hankins, 13-Sep-2009.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎy𝐶    &   ⊢ Ⅎx𝐷    &   ⊢ (x = y → 𝐶 = 𝐷)    ⇒   ⊢ ⦋A / x⦌𝐶 = ⦋A / y⦌𝐷
Theorem	cbvcsbv 2851*	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.)
⊢ (x = y → B = 𝐶)    ⇒   ⊢ ⦋A / x⦌B = ⦋A / y⦌𝐶
Theorem	csbeq1d 2852	Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → ⦋A / x⦌𝐶 = ⦋B / x⦌𝐶)
Theorem	csbid 2853	Analog of sbid 1654 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ ⦋x / x⦌A = A
Theorem	csbeq1a 2854	Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (x = A → B = ⦋A / x⦌B)
Theorem	csbco 2855*	Composition law for chained substitutions into a class. (Contributed by NM, 10-Nov-2005.)
⊢ ⦋A / y⦌⦋y / x⦌B = ⦋A / x⦌B
Theorem	csbtt 2856	Substitution doesn't affect a constant B (in which x is not free). (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ ((A ∈ 𝑉 ∧ ℲxB) → ⦋A / x⦌B = B)
Theorem	csbconstgf 2857	Substitution doesn't affect a constant B (in which x is not free). (Contributed by NM, 10-Nov-2005.)
⊢ ℲxB    ⇒   ⊢ (A ∈ 𝑉 → ⦋A / x⦌B = B)
Theorem	csbconstg 2858*	Substitution doesn't affect a constant B (in which x is not free). csbconstgf 2857 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.)
⊢ (A ∈ 𝑉 → ⦋A / x⦌B = B)
Theorem	sbcel12g 2859	Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (A ∈ 𝑉 → ([A / x]B ∈ 𝐶 ↔ ⦋A / x⦌B ∈ ⦋A / x⦌𝐶))
Theorem	sbceqg 2860	Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (A ∈ 𝑉 → ([A / x]B = 𝐶 ↔ ⦋A / x⦌B = ⦋A / x⦌𝐶))
Theorem	sbcnel12g 2861	Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011.)
⊢ (A ∈ 𝑉 → ([A / x]B ∉ 𝐶 ↔ ⦋A / x⦌B ∉ ⦋A / x⦌𝐶))
Theorem	sbcne12g 2862	Distribute proper substitution through an inequality. (Contributed by Andrew Salmon, 18-Jun-2011.)
⊢ (A ∈ 𝑉 → ([A / x]B ≠ 𝐶 ↔ ⦋A / x⦌B ≠ ⦋A / x⦌𝐶))
Theorem	sbcel1g 2863*	Move proper substitution in and out of a membership relation. Note that the scope of [A / x] is the wff B ∈ 𝐶, whereas the scope of ⦋A / x⦌ is the class B. (Contributed by NM, 10-Nov-2005.)
⊢ (A ∈ 𝑉 → ([A / x]B ∈ 𝐶 ↔ ⦋A / x⦌B ∈ 𝐶))
Theorem	sbceq1g 2864*	Move proper substitution to first argument of an equality. (Contributed by NM, 30-Nov-2005.)
⊢ (A ∈ 𝑉 → ([A / x]B = 𝐶 ↔ ⦋A / x⦌B = 𝐶))
Theorem	sbcel2g 2865*	Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005.)
⊢ (A ∈ 𝑉 → ([A / x]B ∈ 𝐶 ↔ B ∈ ⦋A / x⦌𝐶))
Theorem	sbceq2g 2866*	Move proper substitution to second argument of an equality. (Contributed by NM, 30-Nov-2005.)
⊢ (A ∈ 𝑉 → ([A / x]B = 𝐶 ↔ B = ⦋A / x⦌𝐶))
Theorem	csbcomg 2867*	Commutative law for double substitution into a class. (Contributed by NM, 14-Nov-2005.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → ⦋A / x⦌⦋B / y⦌𝐶 = ⦋B / y⦌⦋A / x⦌𝐶)
Theorem	csbeq2d 2868	Formula-building deduction rule for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ Ⅎxφ    &   ⊢ (φ → B = 𝐶)    ⇒   ⊢ (φ → ⦋A / x⦌B = ⦋A / x⦌𝐶)
Theorem	csbeq2dv 2869*	Formula-building deduction rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ (φ → B = 𝐶)    ⇒   ⊢ (φ → ⦋A / x⦌B = ⦋A / x⦌𝐶)
Theorem	csbeq2i 2870	Formula-building inference rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ B = 𝐶    ⇒   ⊢ ⦋A / x⦌B = ⦋A / x⦌𝐶
Theorem	csbvarg 2871	The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005.)
⊢ (A ∈ 𝑉 → ⦋A / x⦌x = A)
Theorem	sbccsbg 2872*	Substitution into a wff expressed in terms of substitution into a class. (Contributed by NM, 15-Aug-2007.)
⊢ (A ∈ 𝑉 → ([A / x]φ ↔ y ∈ ⦋A / x⦌{y ∣ φ}))
Theorem	sbccsb2g 2873	Substitution into a wff expressed in using substitution into a class. (Contributed by NM, 27-Nov-2005.)
⊢ (A ∈ 𝑉 → ([A / x]φ ↔ A ∈ ⦋A / x⦌{x ∣ φ}))
Theorem	nfcsb1d 2874	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ (φ → ℲxA)    ⇒   ⊢ (φ → Ⅎx⦋A / x⦌B)
Theorem	nfcsb1 2875	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ ℲxA    ⇒   ⊢ Ⅎx⦋A / x⦌B
Theorem	nfcsb1v 2876*	Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎx⦋A / x⦌B
Theorem	nfcsbd 2877	Deduction version of nfcsb 2878. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎyφ    &   ⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx⦋A / y⦌B)
Theorem	nfcsb 2878	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx⦋A / y⦌B
Theorem	csbhypf 2879*	Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 2597 for class substitution version. (Contributed by NM, 19-Dec-2008.)
⊢ ℲxA    &   ⊢ Ⅎx𝐶    &   ⊢ (x = A → B = 𝐶)    ⇒   ⊢ (y = A → ⦋y / x⦌B = 𝐶)
Theorem	csbiebt 2880*	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 2884.) (Contributed by NM, 11-Nov-2005.)
⊢ ((A ∈ 𝑉 ∧ Ⅎx𝐶) → (∀x(x = A → B = 𝐶) ↔ ⦋A / x⦌B = 𝐶))
Theorem	csbiedf 2881*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016.)
⊢ Ⅎxφ    &   ⊢ (φ → Ⅎx𝐶)    &   ⊢ (φ → A ∈ 𝑉)    &   ⊢ ((φ ∧ x = A) → B = 𝐶)    ⇒   ⊢ (φ → ⦋A / x⦌B = 𝐶)
Theorem	csbieb 2882*	Bidirectional conversion between an implicit class substitution hypothesis x = A → B = 𝐶 and its explicit substitution equivalent. (Contributed by NM, 2-Mar-2008.)
⊢ A ∈ V    &   ⊢ Ⅎx𝐶    ⇒   ⊢ (∀x(x = A → B = 𝐶) ↔ ⦋A / x⦌B = 𝐶)
Theorem	csbiebg 2883*	Bidirectional conversion between an implicit class substitution hypothesis x = A → B = 𝐶 and its explicit substitution equivalent. (Contributed by NM, 24-Mar-2013.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎx𝐶    ⇒   ⊢ (A ∈ 𝑉 → (∀x(x = A → B = 𝐶) ↔ ⦋A / x⦌B = 𝐶))
Theorem	csbiegf 2884*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 11-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ (A ∈ 𝑉 → Ⅎx𝐶)    &   ⊢ (x = A → B = 𝐶)    ⇒   ⊢ (A ∈ 𝑉 → ⦋A / x⦌B = 𝐶)
Theorem	csbief 2885*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ A ∈ V    &   ⊢ Ⅎx𝐶    &   ⊢ (x = A → B = 𝐶)    ⇒   ⊢ ⦋A / x⦌B = 𝐶
Theorem	csbied 2886*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ (φ → A ∈ 𝑉)    &   ⊢ ((φ ∧ x = A) → B = 𝐶)    ⇒   ⊢ (φ → ⦋A / x⦌B = 𝐶)
Theorem	csbied2 2887*	Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (φ → A ∈ 𝑉)    &   ⊢ (φ → A = B)    &   ⊢ ((φ ∧ x = B) → 𝐶 = 𝐷)    ⇒   ⊢ (φ → ⦋A / x⦌𝐶 = 𝐷)
Theorem	csbie2t 2888*	Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 2889). (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (∀x∀y((x = A ∧ y = B) → 𝐶 = 𝐷) → ⦋A / x⦌⦋B / y⦌𝐶 = 𝐷)
Theorem	csbie2 2889*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ ((x = A ∧ y = B) → 𝐶 = 𝐷)    ⇒   ⊢ ⦋A / x⦌⦋B / y⦌𝐶 = 𝐷
Theorem	csbie2g 2890*	Conversion of implicit substitution to explicit class substitution. This version of sbcie 2791 avoids a disjointness condition on x and A by substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016.)
⊢ (x = y → B = 𝐶)    &   ⊢ (y = A → 𝐶 = 𝐷)    ⇒   ⊢ (A ∈ 𝑉 → ⦋A / x⦌B = 𝐷)
Theorem	sbcnestgf 2891	Nest the composition of two substitutions. (Contributed by Mario Carneiro, 11-Nov-2016.)
⊢ ((A ∈ 𝑉 ∧ ∀yℲxφ) → ([A / x][B / y]φ ↔ [⦋A / x⦌B / y]φ))
Theorem	csbnestgf 2892	Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
⊢ ((A ∈ 𝑉 ∧ ∀yℲx𝐶) → ⦋A / x⦌⦋B / y⦌𝐶 = ⦋⦋A / x⦌B / y⦌𝐶)
Theorem	sbcnestg 2893*	Nest the composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
⊢ (A ∈ 𝑉 → ([A / x][B / y]φ ↔ [⦋A / x⦌B / y]φ))
Theorem	csbnestg 2894*	Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
⊢ (A ∈ 𝑉 → ⦋A / x⦌⦋B / y⦌𝐶 = ⦋⦋A / x⦌B / y⦌𝐶)
Theorem	csbnest1g 2895	Nest the composition of two substitutions. (Contributed by NM, 23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
⊢ (A ∈ 𝑉 → ⦋A / x⦌⦋B / x⦌𝐶 = ⦋⦋A / x⦌B / x⦌𝐶)
Theorem	csbidmg 2896*	Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.)
⊢ (A ∈ 𝑉 → ⦋A / x⦌⦋A / x⦌B = ⦋A / x⦌B)
Theorem	sbcco3g 2897*	Composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
⊢ (x = A → B = 𝐶)    ⇒   ⊢ (A ∈ 𝑉 → ([A / x][B / y]φ ↔ [𝐶 / y]φ))
Theorem	csbco3g 2898*	Composition of two class substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
⊢ (x = A → B = 𝐶)    ⇒   ⊢ (A ∈ 𝑉 → ⦋A / x⦌⦋B / y⦌𝐷 = ⦋𝐶 / y⦌𝐷)
Theorem	rspcsbela 2899*	Special case related to rspsbc 2834. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.)
⊢ ((A ∈ B ∧ ∀x ∈ B 𝐶 ∈ 𝐷) → ⦋A / x⦌𝐶 ∈ 𝐷)
Theorem	sbnfc2 2900*	Two ways of expressing "x is (effectively) not free in A." (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ (ℲxA ↔ ∀y∀z⦋y / x⦌A = ⦋z / x⦌A)