P. 32 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 3101-3200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sbcbidv 3101*	Formula-building deduction rule for class substitution. (Contributed by NM, 29-Dec-2014.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ([̣A / x]̣ψ ↔ [̣A / x]̣χ))
Theorem	sbcbii 3102	Formula-building inference rule for class substitution. (Contributed by NM, 11-Nov-2005.)
⊢ (φ ↔ ψ)    ⇒   ⊢ ([̣A / x]̣φ ↔ [̣A / x]̣ψ)
Theorem	sbcbiiOLD 3103	Formula-building inference rule for class substitution. (Contributed by NM, 11-Nov-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (A ∈ V → ([̣A / x]̣φ ↔ [̣A / x]̣ψ))
Theorem	eqsbc2 3104*	Substitution for the right-hand side in an equality. This proof was automatically generated from the virtual deduction proof eqsbc2VD in set.mm using a translation program. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ (A ∈ B → ([̣A / x]̣C = x ↔ C = A))
Theorem	sbc3ang 3105	Distribution of class substitution over triple conjunction. (Contributed by NM, 14-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (A ∈ V → ([̣A / x]̣(φ ∧ ψ ∧ χ) ↔ ([̣A / x]̣φ ∧ [̣A / x]̣ψ ∧ [̣A / x]̣χ)))
Theorem	sbcel1gv 3106*	Class substitution into a membership relation. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (A ∈ V → ([̣A / x]̣x ∈ B ↔ A ∈ B))
Theorem	sbcel2gv 3107*	Class substitution into a membership relation. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (B ∈ V → ([̣B / x]̣A ∈ x ↔ A ∈ B))
Theorem	sbcimdv 3108*	Substitution analog of Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 11-Nov-2005.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ ((φ ∧ A ∈ V) → ([̣A / x]̣ψ → [̣A / x]̣χ))
Theorem	sbctt 3109	Substitution for a variable not free in a wff does not affect it. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ ((A ∈ V ∧ Ⅎxφ) → ([̣A / x]̣φ ↔ φ))
Theorem	sbcgf 3110	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 ∈ V → ([̣A / x]̣φ ↔ φ))
Theorem	sbc19.21g 3111	Substitution for a variable not free in antecedent affects only the consequent. (Contributed by NM, 11-Oct-2004.)
⊢ Ⅎxφ    ⇒   ⊢ (A ∈ V → ([̣A / x]̣(φ → ψ) ↔ (φ → [̣A / x]̣ψ)))
Theorem	sbcg 3112*	Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3110. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (A ∈ V → ([̣A / x]̣φ ↔ φ))
Theorem	sbc2iegf 3113*	Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ Ⅎxψ    &   ⊢ Ⅎyψ    &   ⊢ Ⅎx B ∈ W    &   ⊢ ((x = A ∧ y = B) → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ V ∧ B ∈ W) → ([̣A / x]̣[̣B / y]̣φ ↔ ψ))
Theorem	sbc2ie 3114*	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 3115*	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 3116*	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    &   ⊢ C ∈ V    &   ⊢ ((x = A ∧ y = B ∧ z = C) → (φ ↔ ψ))    ⇒   ⊢ ([̣A / x]̣[̣B / y]̣[̣C / z]̣φ ↔ ψ)
Theorem	sbccomlem 3117*	Lemma for sbccom 3118. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 18-Oct-2016.)
⊢ ([̣A / x]̣[̣B / y]̣φ ↔ [̣B / y]̣[̣A / x]̣φ)
Theorem	sbccom 3118*	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 3119*	Interchange class substitution and restricted quantifier. (Contributed by NM, 1-Mar-2008.) (Revised by David Abernethy, 22-Feb-2010.)
⊢ ((A ∈ V ∧ ℲyA) → ([̣A / x]̣∀y ∈ B φ ↔ ∀y ∈ B [̣A / x]̣φ))
Theorem	sbcrext 3120*	Interchange class substitution and restricted existential quantifier. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ ((A ∈ V ∧ ℲyA) → ([̣A / x]̣∃y ∈ B φ ↔ ∃y ∈ B [̣A / x]̣φ))
Theorem	sbcralg 3121*	Interchange class substitution and restricted quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (A ∈ V → ([̣A / x]̣∀y ∈ B φ ↔ ∀y ∈ B [̣A / x]̣φ))
Theorem	sbcrexg 3122*	Interchange class substitution and restricted existential quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (A ∈ V → ([̣A / x]̣∃y ∈ B φ ↔ ∃y ∈ B [̣A / x]̣φ))
Theorem	sbcreug 3123*	Interchange class substitution and restricted uniqueness quantifier. (Contributed by NM, 24-Feb-2013.)
⊢ (A ∈ V → ([̣A / x]̣∃!y ∈ B φ ↔ ∃!y ∈ B [̣A / x]̣φ))
Theorem	sbcabel 3124*	Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005.)
⊢ ℲxB    ⇒   ⊢ (A ∈ V → ([̣A / x]̣{y ∣ φ} ∈ B ↔ {y ∣ [̣A / x]̣φ} ∈ B))
Theorem	rspsbc 3125*	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 2024 and spsbc 3059. See also rspsbca 3126 and rspcsbela 3196. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ (A ∈ B → (∀x ∈ B φ → [̣A / x]̣φ))
Theorem	rspsbca 3126*	Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. (Contributed by NM, 14-Dec-2005.)
⊢ ((A ∈ B ∧ ∀x ∈ B φ) → [̣A / x]̣φ)
Theorem	rspesbca 3127*	Existence form of rspsbca 3126. (Contributed by NM, 29-Feb-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ ((A ∈ B ∧ [̣A / x]̣φ) → ∃x ∈ B φ)
Theorem	spesbc 3128	Existence form of spsbc 3059. (Contributed by Mario Carneiro, 18-Nov-2016.)
⊢ ([̣A / x]̣φ → ∃xφ)
Theorem	spesbcd 3129	form of spsbc 3059. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ (φ → [̣A / x]̣ψ)    ⇒   ⊢ (φ → ∃xψ)
Theorem	sbcth2 3130*	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 3131	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 1798. (Contributed by NM, 16-Jan-2004.)
⊢ Ⅎxφ    ⇒   ⊢ (∀x ∈ A (φ → ψ) → (φ → ∀x ∈ A ψ))
Theorem	rmo2 3132*	Alternate definition of restricted "at most one." Note that ∃*x ∈ Aφ is not equivalent to ∃y ∈ A∀x ∈ A(φ → x = y) (in analogy to reu6 3026); to see this, let A be the empty set. However, one direction of this pattern holds; see rmo2i 3133. (Contributed by NM, 17-Jun-2017.)
⊢ Ⅎyφ    ⇒   ⊢ (∃*x ∈ A φ ↔ ∃y∀x ∈ A (φ → x = y))
Theorem	rmo2i 3133*	Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017.)
⊢ Ⅎyφ    ⇒   ⊢ (∃y ∈ A ∀x ∈ A (φ → x = y) → ∃*x ∈ A φ)
Theorem	rmo3 3134*	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 3135*	Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.)
⊢ (x = B → (φ ↔ ψ))    &   ⊢ (x = C → (φ ↔ χ))    ⇒   ⊢ ((∃*x ∈ A φ ∧ (B ∈ A ∧ ψ)) → (B = C ↔ (C ∈ A ∧ χ)))
Theorem	rmoi 3136*	Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
⊢ (x = B → (φ ↔ ψ))    &   ⊢ (x = C → (φ ↔ χ))    ⇒   ⊢ ((∃*x ∈ A φ ∧ (B ∈ A ∧ ψ) ∧ (C ∈ A ∧ χ)) → B = C)
2.1.9  Proper substitution of classes for sets into classes
Syntax	csb 3137	Extend class notation to include the proper substitution of a class for a set into another class.
class [A / x]B
Definition	df-csb 3138*	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 3047, to prevent ambiguity. Theorem sbcel1g 3156 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3165 recreates substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)
⊢ [A / x]B = {y ∣ [̣A / x]̣y ∈ B}
Theorem	csb2 3139*	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 3140	Analog of dfsbcq 3049 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (A = B → [A / x]C = [B / x]C)
Theorem	cbvcsb 3141	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.)
⊢ ℲyC    &   ⊢ ℲxD    &   ⊢ (x = y → C = D)    ⇒   ⊢ [A / x]C = [A / y]D
Theorem	cbvcsbv 3142*	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 = C)    ⇒   ⊢ [A / x]B = [A / y]C
Theorem	csbeq1d 3143	Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → [A / x]C = [B / x]C)
Theorem	csbid 3144	Analog of sbid 1922 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ [x / x]A = A
Theorem	csbeq1a 3145	Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (x = A → B = [A / x]B)
Theorem	csbco 3146*	Composition law for chained substitutions into a class. (Contributed by NM, 10-Nov-2005.)
⊢ [A / y][y / x]B = [A / x]B
Theorem	csbexg 3147	The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ ((A ∈ V ∧ ∀x B ∈ W) → [A / x]B ∈ V)
Theorem	csbex 3148	The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ [A / x]B ∈ V
Theorem	csbtt 3149	Substitution doesn't affect a constant B (in which x is not free). (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ ((A ∈ V ∧ ℲxB) → [A / x]B = B)
Theorem	csbconstgf 3150	Substitution doesn't affect a constant B (in which x is not free). (Contributed by NM, 10-Nov-2005.)
⊢ ℲxB    ⇒   ⊢ (A ∈ V → [A / x]B = B)
Theorem	csbconstg 3151*	Substitution doesn't affect a constant B (in which x is not free). csbconstgf 3150 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.)
⊢ (A ∈ V → [A / x]B = B)
Theorem	sbcel12g 3152	Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (A ∈ V → ([̣A / x]̣B ∈ C ↔ [A / x]B ∈ [A / x]C))
Theorem	sbceqg 3153	Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (A ∈ V → ([̣A / x]̣B = C ↔ [A / x]B = [A / x]C))
Theorem	sbcnel12g 3154	Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011.)
⊢ (A ∈ V → ([̣A / x]̣B ∉ C ↔ [A / x]B ∉ [A / x]C))
Theorem	sbcne12g 3155	Distribute proper substitution through an inequality. (Contributed by Andrew Salmon, 18-Jun-2011.)
⊢ (A ∈ V → ([̣A / x]̣B ≠ C ↔ [A / x]B ≠ [A / x]C))
Theorem	sbcel1g 3156*	Move proper substitution in and out of a membership relation. Note that the scope of [̣A / x]̣ is the wff B ∈ C, whereas the scope of [A / x] is the class B. (Contributed by NM, 10-Nov-2005.)
⊢ (A ∈ V → ([̣A / x]̣B ∈ C ↔ [A / x]B ∈ C))
Theorem	sbceq1g 3157*	Move proper substitution to first argument of an equality. (Contributed by NM, 30-Nov-2005.)
⊢ (A ∈ V → ([̣A / x]̣B = C ↔ [A / x]B = C))
Theorem	sbcel2g 3158*	Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005.)
⊢ (A ∈ V → ([̣A / x]̣B ∈ C ↔ B ∈ [A / x]C))
Theorem	sbceq2g 3159*	Move proper substitution to second argument of an equality. (Contributed by NM, 30-Nov-2005.)
⊢ (A ∈ V → ([̣A / x]̣B = C ↔ B = [A / x]C))
Theorem	csbcomg 3160*	Commutative law for double substitution into a class. (Contributed by NM, 14-Nov-2005.)
⊢ ((A ∈ V ∧ B ∈ W) → [A / x][B / y]C = [B / y][A / x]C)
Theorem	csbeq2d 3161	Formula-building deduction rule for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ Ⅎxφ    &   ⊢ (φ → B = C)    ⇒   ⊢ (φ → [A / x]B = [A / x]C)
Theorem	csbeq2dv 3162*	Formula-building deduction rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ (φ → B = C)    ⇒   ⊢ (φ → [A / x]B = [A / x]C)
Theorem	csbeq2i 3163	Formula-building inference rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ B = C    ⇒   ⊢ [A / x]B = [A / x]C
Theorem	csbvarg 3164	The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005.)
⊢ (A ∈ V → [A / x]x = A)
Theorem	sbccsbg 3165*	Substitution into a wff expressed in terms of substitution into a class. (Contributed by NM, 15-Aug-2007.)
⊢ (A ∈ V → ([̣A / x]̣φ ↔ y ∈ [A / x]{y ∣ φ}))
Theorem	sbccsb2g 3166	Substitution into a wff expressed in using substitution into a class. (Contributed by NM, 27-Nov-2005.)
⊢ (A ∈ V → ([̣A / x]̣φ ↔ A ∈ [A / x]{x ∣ φ}))
Theorem	nfcsb1d 3167	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ (φ → ℲxA)    ⇒   ⊢ (φ → Ⅎx[A / x]B)
Theorem	nfcsb1 3168	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ ℲxA    ⇒   ⊢ Ⅎx[A / x]B
Theorem	nfcsb1v 3169*	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 3170	Deduction version of nfcsb 3171. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎyφ    &   ⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx[A / y]B)
Theorem	nfcsb 3171	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx[A / y]B
Theorem	csbhypf 3172*	Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 2905 for class substitution version. (Contributed by NM, 19-Dec-2008.)
⊢ ℲxA    &   ⊢ ℲxC    &   ⊢ (x = A → B = C)    ⇒   ⊢ (y = A → [y / x]B = C)
Theorem	csbiebt 3173*	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3177.) (Contributed by NM, 11-Nov-2005.)
⊢ ((A ∈ V ∧ ℲxC) → (∀x(x = A → B = C) ↔ [A / x]B = C))
Theorem	csbiedf 3174*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016.)
⊢ Ⅎxφ    &   ⊢ (φ → ℲxC)    &   ⊢ (φ → A ∈ V)    &   ⊢ ((φ ∧ x = A) → B = C)    ⇒   ⊢ (φ → [A / x]B = C)
Theorem	csbieb 3175*	Bidirectional conversion between an implicit class substitution hypothesis x = A → B = C and its explicit substitution equivalent. (Contributed by NM, 2-Mar-2008.)
⊢ A ∈ V    &   ⊢ ℲxC    ⇒   ⊢ (∀x(x = A → B = C) ↔ [A / x]B = C)
Theorem	csbiebg 3176*	Bidirectional conversion between an implicit class substitution hypothesis x = A → B = C and its explicit substitution equivalent. (Contributed by NM, 24-Mar-2013.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ ℲxC    ⇒   ⊢ (A ∈ V → (∀x(x = A → B = C) ↔ [A / x]B = C))
Theorem	csbiegf 3177*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 11-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ (A ∈ V → ℲxC)    &   ⊢ (x = A → B = C)    ⇒   ⊢ (A ∈ V → [A / x]B = C)
Theorem	csbief 3178*	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    &   ⊢ ℲxC    &   ⊢ (x = A → B = C)    ⇒   ⊢ [A / x]B = C
Theorem	csbied 3179*	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 ∈ V)    &   ⊢ ((φ ∧ x = A) → B = C)    ⇒   ⊢ (φ → [A / x]B = C)
Theorem	csbied2 3180*	Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (φ → A ∈ V)    &   ⊢ (φ → A = B)    &   ⊢ ((φ ∧ x = B) → C = D)    ⇒   ⊢ (φ → [A / x]C = D)
Theorem	csbie2t 3181*	Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 3182). (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (∀x∀y((x = A ∧ y = B) → C = D) → [A / x][B / y]C = D)
Theorem	csbie2 3182*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ ((x = A ∧ y = B) → C = D)    ⇒   ⊢ [A / x][B / y]C = D
Theorem	csbie2g 3183*	Conversion of implicit substitution to explicit class substitution. This version of sbcie 3081 avoids a disjointness condition on x, A by substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016.)
⊢ (x = y → B = C)    &   ⊢ (y = A → C = D)    ⇒   ⊢ (A ∈ V → [A / x]B = D)
Theorem	sbcnestgf 3184	Nest the composition of two substitutions. (Contributed by Mario Carneiro, 11-Nov-2016.)
⊢ ((A ∈ V ∧ ∀yℲxφ) → ([̣A / x]̣[̣B / y]̣φ ↔ [̣[A / x]B / y]̣φ))
Theorem	csbnestgf 3185	Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
⊢ ((A ∈ V ∧ ∀yℲxC) → [A / x][B / y]C = [[A / x]B / y]C)
Theorem	sbcnestg 3186*	Nest the composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
⊢ (A ∈ V → ([̣A / x]̣[̣B / y]̣φ ↔ [̣[A / x]B / y]̣φ))
Theorem	csbnestg 3187*	Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
⊢ (A ∈ V → [A / x][B / y]C = [[A / x]B / y]C)
Theorem	csbnestgOLD 3188*	Nest the composition of two substitutions. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by NM, 23-Nov-2005.)
⊢ ((A ∈ V ∧ ∀x B ∈ W) → [A / x][B / y]C = [[A / x]B / y]C)
Theorem	csbnest1g 3189	Nest the composition of two substitutions. (Contributed by NM, 23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
⊢ (A ∈ V → [A / x][B / x]C = [[A / x]B / x]C)
Theorem	csbnest1gOLD 3190*	Nest the composition of two substitutions. Obsolete as of 11-Nov-2016. (Contributed by NM, 23-May-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((A ∈ V ∧ ∀x B ∈ W) → [A / x][B / x]C = [[A / x]B / x]C)
Theorem	csbidmg 3191*	Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.)
⊢ (A ∈ V → [A / x][A / x]B = [A / x]B)
Theorem	sbcco3g 3192*	Composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
⊢ (x = A → B = C)    ⇒   ⊢ (A ∈ V → ([̣A / x]̣[̣B / y]̣φ ↔ [̣C / y]̣φ))
Theorem	sbcco3gOLD 3193*	Composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (x = A → B = C)    ⇒   ⊢ ((A ∈ V ∧ ∀x B ∈ W) → ([̣A / x]̣[̣B / y]̣φ ↔ [̣C / y]̣φ))
Theorem	csbco3g 3194*	Composition of two class substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
⊢ (x = A → B = C)    ⇒   ⊢ (A ∈ V → [A / x][B / y]D = [C / y]D)
Theorem	csbco3gOLD 3195*	Composition of two class substitutions. Obsolete as of 11-Nov-2016. (Contributed by NM, 27-Nov-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (x = A → B = D)    ⇒   ⊢ ((A ∈ V ∧ ∀x B ∈ W) → [A / x][B / y]C = [D / y]C)
Theorem	rspcsbela 3196*	Special case related to rspsbc 3125. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.)
⊢ ((A ∈ B ∧ ∀x ∈ B C ∈ D) → [A / x]C ∈ D)
Theorem	sbnfc2 3197*	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)
Theorem	csbabg 3198*	Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (A ∈ V → [A / x]{y ∣ φ} = {y ∣ [̣A / x]̣φ})
Theorem	cbvralcsf 3199	A more general version of cbvralf 2830 that doesn't require A and B to be distinct from x or y. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.)
⊢ ℲyA    &   ⊢ ℲxB    &   ⊢ Ⅎyφ    &   ⊢ Ⅎxψ    &   ⊢ (x = y → A = B)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∀x ∈ A φ ↔ ∀y ∈ B ψ)
Theorem	cbvrexcsf 3200	A more general version of cbvrexf 2831 that has no distinct variable restrictions. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.) (Proof shortened by Mario Carneiro, 7-Dec-2014.)
⊢ ℲyA    &   ⊢ ℲxB    &   ⊢ Ⅎyφ    &   ⊢ Ⅎxψ    &   ⊢ (x = y → A = B)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ A φ ↔ ∃y ∈ B ψ)