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	sbcbii 3101	Formula-building inference rule for class substitution. (Contributed by NM, 11-Nov-2005.)
⊢ (φ ↔ ψ)    ⇒   ⊢ ([̣A / x]̣φ ↔ [̣A / x]̣ψ)
Theorem	sbcbiiOLD 3102	Formula-building inference rule for class substitution. (Contributed by NM, 11-Nov-2005.) (New usage is discouraged.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (A ∈ V → ([̣A / x]̣φ ↔ [̣A / x]̣ψ))
Theorem	eqsbc3r 3103*	eqsbc3 3085 with setvar variable on right side of equals sign. This proof was automatically generated from the virtual deduction proof eqsbc3rVD in set.mm using a translation program. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ (A ∈ B → ([̣A / x]̣C = x ↔ C = A))
Theorem	sbc3ang 3104	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 3105*	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 3106*	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 3107*	Substitution analog of Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 11-Nov-2005.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ ((φ ∧ A ∈ V) → ([̣A / x]̣ψ → [̣A / x]̣χ))
Theorem	sbctt 3108	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 3109	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 3110	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 3111*	Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3109. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (A ∈ V → ([̣A / x]̣φ ↔ φ))
Theorem	sbc2iegf 3112*	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 3113*	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 3114*	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 3115*	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 3116*	Lemma for sbccom 3117. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 18-Oct-2016.)
⊢ ([̣A / x]̣[̣B / y]̣φ ↔ [̣B / y]̣[̣A / x]̣φ)
Theorem	sbccom 3117*	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 3118*	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 3119*	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 3120*	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 3121*	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 3122*	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 3123*	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 3124*	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 3058. See also rspsbca 3125 and rspcsbela 3195. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ (A ∈ B → (∀x ∈ B φ → [̣A / x]̣φ))
Theorem	rspsbca 3125*	Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. (Contributed by NM, 14-Dec-2005.)
⊢ ((A ∈ B ∧ ∀x ∈ B φ) → [̣A / x]̣φ)
Theorem	rspesbca 3126*	Existence form of rspsbca 3125. (Contributed by NM, 29-Feb-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ ((A ∈ B ∧ [̣A / x]̣φ) → ∃x ∈ B φ)
Theorem	spesbc 3127	Existence form of spsbc 3058. (Contributed by Mario Carneiro, 18-Nov-2016.)
⊢ ([̣A / x]̣φ → ∃xφ)
Theorem	spesbcd 3128	form of spsbc 3058. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ (φ → [̣A / x]̣ψ)    ⇒   ⊢ (φ → ∃xψ)
Theorem	sbcth2 3129*	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 3130	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 3131*	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 3025); to see this, let A be the empty set. However, one direction of this pattern holds; see rmo2i 3132. (Contributed by NM, 17-Jun-2017.)
⊢ Ⅎyφ    ⇒   ⊢ (∃*x ∈ A φ ↔ ∃y∀x ∈ A (φ → x = y))
Theorem	rmo2i 3132*	Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017.)
⊢ Ⅎyφ    ⇒   ⊢ (∃y ∈ A ∀x ∈ A (φ → x = y) → ∃*x ∈ A φ)
Theorem	rmo3 3133*	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 3134*	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 3135*	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 3136	Extend class notation to include the proper substitution of a class for a set into another class.
class [A / x]B
Definition	df-csb 3137*	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 3046, to prevent ambiguity. Theorem sbcel1g 3155 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3164 recreates substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)
⊢ [A / x]B = {y ∣ [̣A / x]̣y ∈ B}
Theorem	csb2 3138*	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 3139	Analog of dfsbcq 3048 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (A = B → [A / x]C = [B / x]C)
Theorem	cbvcsb 3140	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 3141*	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 3142	Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → [A / x]C = [B / x]C)
Theorem	csbid 3143	Analog of sbid 1922 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ [x / x]A = A
Theorem	csbeq1a 3144	Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (x = A → B = [A / x]B)
Theorem	csbco 3145*	Composition law for chained substitutions into a class. (Contributed by NM, 10-Nov-2005.)
⊢ [A / y][y / x]B = [A / x]B
Theorem	csbexg 3146	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 3147	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 3148	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 3149	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 3150*	Substitution doesn't affect a constant B (in which x is not free). csbconstgf 3149 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.)
⊢ (A ∈ V → [A / x]B = B)
Theorem	sbcel12g 3151	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 3152	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 3153	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 3154	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 3155*	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 3156*	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 3157*	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 3158*	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 3159*	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 3160	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 3161*	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 3162	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 3163	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 3164*	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 3165	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 3166	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ (φ → ℲxA)    ⇒   ⊢ (φ → Ⅎx[A / x]B)
Theorem	nfcsb1 3167	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ ℲxA    ⇒   ⊢ Ⅎx[A / x]B
Theorem	nfcsb1v 3168*	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 3169	Deduction version of nfcsb 3170. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎyφ    &   ⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx[A / y]B)
Theorem	nfcsb 3170	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx[A / y]B
Theorem	csbhypf 3171*	Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 2904 for class substitution version. (Contributed by NM, 19-Dec-2008.)
⊢ ℲxA    &   ⊢ ℲxC    &   ⊢ (x = A → B = C)    ⇒   ⊢ (y = A → [y / x]B = C)
Theorem	csbiebt 3172*	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3176.) (Contributed by NM, 11-Nov-2005.)
⊢ ((A ∈ V ∧ ℲxC) → (∀x(x = A → B = C) ↔ [A / x]B = C))
Theorem	csbiedf 3173*	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 3174*	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 3175*	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 3176*	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 3177*	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 3178*	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 3179*	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 3180*	Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 3181). (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 3181*	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 3182*	Conversion of implicit substitution to explicit class substitution. This version of sbcie 3080 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 3183	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 3184	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 3185*	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 3186*	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 3187*	Nest the composition of two substitutions. (New usage 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 3188	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 3189*	Nest the composition of two substitutions. Obsolete as of 11-Nov-2016. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
⊢ ((A ∈ V ∧ ∀x B ∈ W) → [A / x][B / x]C = [[A / x]B / x]C)
Theorem	csbidmg 3190*	Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.)
⊢ (A ∈ V → [A / x][A / x]B = [A / x]B)
Theorem	sbcco3g 3191*	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 3192*	Composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (New usage is discouraged.)
⊢ (x = A → B = C)    ⇒   ⊢ ((A ∈ V ∧ ∀x B ∈ W) → ([̣A / x]̣[̣B / y]̣φ ↔ [̣C / y]̣φ))
Theorem	csbco3g 3193*	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 3194*	Composition of two class substitutions. Obsolete as of 11-Nov-2016. (Contributed by NM, 27-Nov-2005.) (New usage is discouraged.)
⊢ (x = A → B = D)    ⇒   ⊢ ((A ∈ V ∧ ∀x B ∈ W) → [A / x][B / y]C = [D / y]C)
Theorem	rspcsbela 3195*	Special case related to rspsbc 3124. (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 3196*	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 3197*	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 3198	A more general version of cbvralf 2829 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 3199	A more general version of cbvrexf 2830 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 ψ)
Theorem	cbvreucsf 3200	A more general version of cbvreuv 2837 that has no distinct variable rextrictions. 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 ψ)