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.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> ( [.A / x ].ps <-> [.A / x ].ch))
Theorem	sbcbii 3102	Formula-building inference rule for class substitution. (Contributed by NM, 11-Nov-2005.)
|- (ph <-> ps)   =>   |- ( [.A / x ].ph <-> [.A / x ].ps)
Theorem	sbcbiiOLD 3103	Formula-building inference rule for class substitution. (Contributed by NM, 11-Nov-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (ph <-> ps)   =>   |- (A e. V -> ( [.A / x ].ph <-> [.A / x ].ps))
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 e. 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 e. V -> ( [.A / x ].(ph /\ ps /\ ch) <-> ( [.A / x ].ph /\ [.A / x ].ps /\ [.A / x ].ch)))
Theorem	sbcel1gv 3106*	Class substitution into a membership relation. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- (A e. V -> ( [.A / x ].x e. B <-> A e. 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 e. V -> ( [.B / x ].A e. x <-> A e. B))
Theorem	sbcimdv 3108*	Substitution analog of Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 11-Nov-2005.)
|- (ph -> (ps -> ch))   =>   |- ((ph /\ A e. V) -> ( [.A / x ].ps -> [.A / x ].ch))
Theorem	sbctt 3109	Substitution for a variable not free in a wff does not affect it. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- ((A e. V /\ F/xph) -> ( [.A / x ].ph <-> ph))
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.)
|- F/xph   =>   |- (A e. V -> ( [.A / x ].ph <-> ph))
Theorem	sbc19.21g 3111	Substitution for a variable not free in antecedent affects only the consequent. (Contributed by NM, 11-Oct-2004.)
|- F/xph   =>   |- (A e. V -> ( [.A / x ].(ph -> ps) <-> (ph -> [.A / x ].ps)))
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 e. V -> ( [.A / x ].ph <-> ph))
Theorem	sbc2iegf 3113*	Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Dec-2013.)
|- F/xps   &   |- F/yps   &   |- F/x B e. W   &   |- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- ((A e. V /\ B e. W) -> ( [.A / x ]. [.B / y ].ph <-> ps))
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 e. _V   &   |- B e. _V   &   |- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- ( [.A / x ]. [.B / y ].ph <-> ps)
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 e. _V   &   |- B e. _V   &   |- (ph -> ((x = A /\ y = B) -> (ps <-> ch)))   =>   |- (ph -> ( [.A / x ]. [.B / y ].ps <-> ch))
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 e. _V   &   |- B e. _V   &   |- C e. _V   &   |- ((x = A /\ y = B /\ z = C) -> (ph <-> ps))   =>   |- ( [.A / x ]. [.B / y ]. [.C / z ].ph <-> ps)
Theorem	sbccomlem 3117*	Lemma for sbccom 3118. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 18-Oct-2016.)
|- ( [.A / x ]. [.B / y ].ph <-> [.B / y ]. [.A / x ].ph)
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 ].ph <-> [.B / y ]. [.A / x ].ph)
Theorem	sbcralt 3119*	Interchange class substitution and restricted quantifier. (Contributed by NM, 1-Mar-2008.) (Revised by David Abernethy, 22-Feb-2010.)
|- ((A e. V /\ F/_yA) -> ( [.A / x ].A.y e. B ph <-> A.y e. B [.A / x ].ph))
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 e. V /\ F/_yA) -> ( [.A / x ].E.y e. B ph <-> E.y e. B [.A / x ].ph))
Theorem	sbcralg 3121*	Interchange class substitution and restricted quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- (A e. V -> ( [.A / x ].A.y e. B ph <-> A.y e. B [.A / x ].ph))
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 e. V -> ( [.A / x ].E.y e. B ph <-> E.y e. B [.A / x ].ph))
Theorem	sbcreug 3123*	Interchange class substitution and restricted uniqueness quantifier. (Contributed by NM, 24-Feb-2013.)
|- (A e. V -> ( [.A / x ].E!y e. B ph <-> E!y e. B [.A / x ].ph))
Theorem	sbcabel 3124*	Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005.)
|- F/_xB   =>   |- (A e. V -> ( [.A / x ].{y | ph} e. B <-> {y | [.A / x ].ph} e. 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 e. B -> (A.x e. B ph -> [.A / x ].ph))
Theorem	rspsbca 3126*	Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. (Contributed by NM, 14-Dec-2005.)
|- ((A e. B /\ A.x e. B ph) -> [.A / x ].ph)
Theorem	rspesbca 3127*	Existence form of rspsbca 3126. (Contributed by NM, 29-Feb-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
|- ((A e. B /\ [.A / x ].ph) -> E.x e. B ph)
Theorem	spesbc 3128	Existence form of spsbc 3059. (Contributed by Mario Carneiro, 18-Nov-2016.)
|- ( [.A / x ].ph -> E.xph)
Theorem	spesbcd 3129	form of spsbc 3059. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- (ph -> [.A / x ].ps)   =>   |- (ph -> E.xps)
Theorem	sbcth2 3130*	A substitution into a theorem. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
|- (x e. B -> ph)   =>   |- (A e. B -> [.A / x ].ph)
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.)
|- F/xph   =>   |- (A.x e. A (ph -> ps) -> (ph -> A.x e. A ps))
Theorem	rmo2 3132*	Alternate definition of restricted "at most one." Note that E*x e. Aph is not equivalent to E.y e. AA.x e. A(ph -> 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.)
|- F/yph   =>   |- (E*x e. A ph <-> E.yA.x e. A (ph -> x = y))
Theorem	rmo2i 3133*	Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017.)
|- F/yph   =>   |- (E.y e. A A.x e. A (ph -> x = y) -> E*x e. A ph)
Theorem	rmo3 3134*	Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
|- F/yph   =>   |- (E*x e. A ph <-> A.x e. A A.y e. A ((ph /\ [y / x]ph) -> 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 -> (ph <-> ps))   &   |- (x = C -> (ph <-> ch))   =>   |- ((E*x e. A ph /\ (B e. A /\ ps)) -> (B = C <-> (C e. A /\ ch)))
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 -> (ph <-> ps))   &   |- (x = C -> (ph <-> ch))   =>   |- ((E*x e. A ph /\ (B e. A /\ ps) /\ (C e. A /\ ch)) -> 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 e. 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 | E.x(x = A /\ y e. 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.)
|- F/_yC   &   |- F/_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.)
|- (ph -> A = B)   =>   |- (ph -> [_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 e. V /\ A.x B e. W) -> [_A / x]_B e. _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 e. _V   &   |- B e. _V   =>   |- [_A / x]_B e. _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 e. V /\ F/_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.)
|- F/_xB   =>   |- (A e. 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 e. 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 e. V -> ( [.A / x ].B e. C <-> [_A / x]_B e. [_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 e. 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 e. V -> ( [.A / x ].B e/ C <-> [_A / x]_B e/ [_A / x]_C))
Theorem	sbcne12g 3155	Distribute proper substitution through an inequality. (Contributed by Andrew Salmon, 18-Jun-2011.)
|- (A e. 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 e. C, whereas the scope of [_A / x]_ is the class B. (Contributed by NM, 10-Nov-2005.)
|- (A e. V -> ( [.A / x ].B e. C <-> [_A / x]_B e. C))
Theorem	sbceq1g 3157*	Move proper substitution to first argument of an equality. (Contributed by NM, 30-Nov-2005.)
|- (A e. 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 e. V -> ( [.A / x ].B e. C <-> B e. [_A / x]_C))
Theorem	sbceq2g 3159*	Move proper substitution to second argument of an equality. (Contributed by NM, 30-Nov-2005.)
|- (A e. 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 e. V /\ B e. 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.)
|- F/xph   &   |- (ph -> B = C)   =>   |- (ph -> [_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.)
|- (ph -> B = C)   =>   |- (ph -> [_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 e. 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 e. V -> ( [.A / x ].ph <-> y e. [_A / x]_{y | ph}))
Theorem	sbccsb2g 3166	Substitution into a wff expressed in using substitution into a class. (Contributed by NM, 27-Nov-2005.)
|- (A e. V -> ( [.A / x ].ph <-> A e. [_A / x]_{x | ph}))
Theorem	nfcsb1d 3167	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
|- (ph -> F/_xA)   =>   |- (ph -> F/_x[_A / x]_B)
Theorem	nfcsb1 3168	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
|- F/_xA   =>   |- F/_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.)
|- F/_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.)
|- F/yph   &   |- (ph -> F/_xA)   &   |- (ph -> F/_xB)   =>   |- (ph -> F/_x[_A / y]_B)
Theorem	nfcsb 3171	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
|- F/_xA   &   |- F/_xB   =>   |- F/_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.)
|- F/_xA   &   |- F/_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 e. V /\ F/_xC) -> (A.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.)
|- F/xph   &   |- (ph -> F/_xC)   &   |- (ph -> A e. V)   &   |- ((ph /\ x = A) -> B = C)   =>   |- (ph -> [_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 e. _V   &   |- F/_xC   =>   |- (A.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.)
|- F/_xC   =>   |- (A e. V -> (A.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 e. V -> F/_xC)   &   |- (x = A -> B = C)   =>   |- (A e. 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 e. _V   &   |- F/_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.)
|- (ph -> A e. V)   &   |- ((ph /\ x = A) -> B = C)   =>   |- (ph -> [_A / x]_B = C)
Theorem	csbied2 3180*	Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- (ph -> A e. V)   &   |- (ph -> A = B)   &   |- ((ph /\ x = B) -> C = D)   =>   |- (ph -> [_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 e. _V   &   |- B e. _V   =>   |- (A.xA.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 e. _V   &   |- B e. _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 e. V -> [_A / x]_B = D)
Theorem	sbcnestgf 3184	Nest the composition of two substitutions. (Contributed by Mario Carneiro, 11-Nov-2016.)
|- ((A e. V /\ A.y F/xph) -> ( [.A / x ]. [.B / y ].ph <-> [.[_A / x]_B / y ].ph))
Theorem	csbnestgf 3185	Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
|- ((A e. V /\ A.y F/_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 e. V -> ( [.A / x ]. [.B / y ].ph <-> [.[_A / x]_B / y ].ph))
Theorem	csbnestg 3187*	Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
|- (A e. 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 e. V /\ A.x B e. 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 e. 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 e. V /\ A.x B e. 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 e. 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 e. V -> ( [.A / x ]. [.B / y ].ph <-> [.C / y ].ph))
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 e. V /\ A.x B e. W) -> ( [.A / x ]. [.B / y ].ph <-> [.C / y ].ph))
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 e. 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 e. V /\ A.x B e. 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 e. B /\ A.x e. B C e. D) -> [_A / x]_C e. D)
Theorem	sbnfc2 3197*	Two ways of expressing "x is (effectively) not free in A." (Contributed by Mario Carneiro, 14-Oct-2016.)
|- ( F/_xA <-> A.yA.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 e. V -> [_A / x]_{y | ph} = {y | [.A / x ].ph})
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.)
|- F/_yA   &   |- F/_xB   &   |- F/yph   &   |- F/xps   &   |- (x = y -> A = B)   &   |- (x = y -> (ph <-> ps))   =>   |- (A.x e. A ph <-> A.y e. B ps)
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.)
|- F/_yA   &   |- F/_xB   &   |- F/yph   &   |- F/xps   &   |- (x = y -> A = B)   &   |- (x = y -> (ph <-> ps))   =>   |- (E.x e. A ph <-> E.y e. B ps)