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.)
|- (ph <-> ps)   =>   |- ( [.A / x ].ph <-> [.A / x ].ps)
Theorem	sbcbiiOLD 3102	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	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 e. 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 e. V -> ( [.A / x ].(ph /\ ps /\ ch) <-> ( [.A / x ].ph /\ [.A / x ].ps /\ [.A / x ].ch)))
Theorem	sbcel1gv 3105*	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 3106*	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 3107*	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 3108	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 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.)
|- F/xph   =>   |- (A e. V -> ( [.A / x ].ph <-> ph))
Theorem	sbc19.21g 3110	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 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 e. V -> ( [.A / x ].ph <-> ph))
Theorem	sbc2iegf 3112*	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 3113*	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 3114*	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 3115*	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 3116*	Lemma for sbccom 3117. (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 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 ].ph <-> [.B / y ]. [.A / x ].ph)
Theorem	sbcralt 3118*	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 3119*	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 3120*	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 3121*	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 3122*	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 3123*	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 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 e. B -> (A.x e. B ph -> [.A / x ].ph))
Theorem	rspsbca 3125*	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 3126*	Existence form of rspsbca 3125. (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 3127	Existence form of spsbc 3058. (Contributed by Mario Carneiro, 18-Nov-2016.)
|- ( [.A / x ].ph -> E.xph)
Theorem	spesbcd 3128	form of spsbc 3058. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- (ph -> [.A / x ].ps)   =>   |- (ph -> E.xps)
Theorem	sbcth2 3129*	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 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.)
|- F/xph   =>   |- (A.x e. A (ph -> ps) -> (ph -> A.x e. A ps))
Theorem	rmo2 3131*	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 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.)
|- F/yph   =>   |- (E*x e. A ph <-> E.yA.x e. A (ph -> x = y))
Theorem	rmo2i 3132*	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 3133*	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 3134*	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 3135*	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 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 e. 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 | E.x(x = A /\ y e. 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.)
|- F/_yC   &   |- F/_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.)
|- (ph -> A = B)   =>   |- (ph -> [_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 e. V /\ A.x B e. W) -> [_A / x]_B e. _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 e. _V   &   |- B e. _V   =>   |- [_A / x]_B e. _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 e. V /\ F/_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.)
|- F/_xB   =>   |- (A e. 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 e. 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 e. V -> ( [.A / x ].B e. C <-> [_A / x]_B e. [_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 e. 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 e. V -> ( [.A / x ].B e/ C <-> [_A / x]_B e/ [_A / x]_C))
Theorem	sbcne12g 3154	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 3155*	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 3156*	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 3157*	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 3158*	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 3159*	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 3160	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 3161*	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 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 e. 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 e. V -> ( [.A / x ].ph <-> y e. [_A / x]_{y | ph}))
Theorem	sbccsb2g 3165	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 3166	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 3167	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 3168*	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 3169	Deduction version of nfcsb 3170. (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 3170	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 3171*	Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 2904 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 3172*	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3176.) (Contributed by NM, 11-Nov-2005.)
|- ((A e. V /\ F/_xC) -> (A.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.)
|- F/xph   &   |- (ph -> F/_xC)   &   |- (ph -> A e. V)   &   |- ((ph /\ x = A) -> B = C)   =>   |- (ph -> [_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 e. _V   &   |- F/_xC   =>   |- (A.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.)
|- F/_xC   =>   |- (A e. V -> (A.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 e. V -> F/_xC)   &   |- (x = A -> B = C)   =>   |- (A e. 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 e. _V   &   |- F/_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.)
|- (ph -> A e. V)   &   |- ((ph /\ x = A) -> B = C)   =>   |- (ph -> [_A / x]_B = C)
Theorem	csbied2 3179*	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 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 e. _V   &   |- B e. _V   =>   |- (A.xA.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 e. _V   &   |- B e. _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 e. V -> [_A / x]_B = D)
Theorem	sbcnestgf 3183	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 3184	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 3185*	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 3186*	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 3187*	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 3188	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 3189*	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 3190*	Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.)
|- (A e. 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 e. V -> ( [.A / x ]. [.B / y ].ph <-> [.C / y ].ph))
Theorem	sbcco3gOLD 3192*	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 3193*	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 3194*	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 3195*	Special case related to rspsbc 3124. (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 3196*	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 3197*	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 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.)
|- 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 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.)
|- 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)
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.)
|- 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)