P. 32 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3101-3200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sbcbidv 3101*	Formula-building deduction 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 for class substitution. (Contributed by NM, 11-Nov-2005.)
|- ( ph <-> ps )   =>    |- ( [. A / x ]. ph <-> [. A / x ]. ps )
Theorem	eqsbc2 3103*	Substitution for the right-hand side in an equality. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by JJ, 7-Jul-2021.)
|- ( A e. V -> ( [. A / x ]. B = x <-> B = A ) )
Theorem	sbc3an 3104	Distribution of class substitution over triple conjunction. (Contributed by NM, 14-Dec-2006.) (Revised by NM, 17-Aug-2018.)
|- ( [. A / x ]. ( ph /\ ps /\ ch ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps /\ [. A / x ]. ch ) )
Theorem	sbcel1v 3105*	Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.)
|- ( [. 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	sbcel21v 3107*	Class substitution into a membership relation. One direction of sbcel2gv 3106 that holds for proper classes. (Contributed by NM, 17-Aug-2018.)
|- ( [. B / x ]. A e. x -> A e. B )
Theorem	sbcimdv 3108*	Substitution analogue of Theorem 19.20 of [Margaris] p. 90 (alim 1506). (Contributed by NM, 11-Nov-2005.) (Revised by NM, 17-Aug-2018.) (Proof shortened by JJ, 7-Jul-2021.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( [. 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/ x ph ) -> ( [. 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/ x ph   =>    |- ( 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/ x ph   =>    |- ( 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/ x ps   &    |- F/ y ps   &    |- 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/_ y A ) -> ( [. 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.)
|- ( F/_ y A -> ( [. 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	sbcrex 3122*	Interchange class substitution and restricted existential quantifier. (Contributed by NM, 15-Nov-2005.) (Revised by NM, 18-Aug-2018.)
|- ( [. A / x ]. E. y e. B ph <-> E. y e. B [. A / x ]. ph )
Theorem	sbcreug 3123*	Interchange class substitution and restricted unique existential 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	reu8nf 3124*	Restricted uniqueness using implicit substitution. This version of reu8 3013 uses a nonfreeness hypothesis for x and ps instead of distinct variable conditions. (Contributed by AV, 21-Jan-2022.)
|- F/ x ps   &    |- F/ x ch   &    |- ( x = w -> ( ph <-> ch ) )   &    |- ( w = y -> ( ch <-> ps ) )   =>    |- ( E! x e. A ph <-> E. x e. A ( ph /\ A. y e. A ( ps -> x = y ) ) )
Theorem	sbcabel 3125*	Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005.)
|- F/_ x B   =>    |- ( A e. V -> ( [. A / x ]. { y | ph } e. B <-> { y | [. A / x ]. ph } e. B ) )
Theorem	rspsbc 3126*	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 1824 and spsbc 3054. See also rspsbca 3127 and rspcsbela . (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 3127*	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 3128*	Existence form of rspsbca 3127. (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 3129	Existence form of spsbc 3054. (Contributed by Mario Carneiro, 18-Nov-2016.)
|- ( [. A / x ]. ph -> E. x ph )
Theorem	spesbcd 3130	form of spsbc 3054. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ph -> [. A / x ]. ps )   =>    |- ( ph -> E. x ps )
Theorem	sbcth2 3131*	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 3132	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 1633. (Contributed by NM, 16-Jan-2004.)
|- F/ x ph   =>    |- ( A. x e. A ( ph -> ps ) -> ( ph -> A. x e. A ps ) )
Theorem	rmo2ilem 3133*	Condition implying restricted at-most-one quantifier. (Contributed by Jim Kingdon, 14-Jul-2018.)
|- F/ y ph   =>    |- ( E. y A. x e. A ( ph -> x = y ) -> E* x e. A ph )
Theorem	rmo2i 3134*	Condition implying restricted at-most-one quantifier. (Contributed by NM, 17-Jun-2017.)
|- F/ y ph   =>    |- ( E. y e. A A. x e. A ( ph -> x = y ) -> E* x e. A ph )
Theorem	rmo3 3135*	Restricted at-most-one quantifier using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
|- F/ y ph   =>    |- ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) )
Theorem	rmob 3136*	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 3137*	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.10  Proper substitution of classes for sets into classes
Syntax	csb 3138	Extend class notation to include the proper substitution of a class for a set into another class.
class [_ A / x ]_ B
Definition	df-csb 3139*	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 3042, to prevent ambiguity. Theorem sbcel1g 3157 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3167 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 3140*	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 3141	Analog of dfsbcq 3044 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
|- ( A = B -> [_ A / x ]_ C = [_ B / x ]_ C )
Theorem	cbvcsbw 3142*	Version of cbvcsb 3143 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.)
|- F/_ y C   &    |- F/_ x D   &    |- ( x = y -> C = D )   =>    |- [_ A / x ]_ C = [_ A / y ]_ D
Theorem	cbvcsb 3143	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/_ y C   &    |- F/_ x D   &    |- ( x = y -> C = D )   =>    |- [_ A / x ]_ C = [_ A / y ]_ D
Theorem	cbvcsbv 3144*	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 3145	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 3146	Analog of sbid 1823 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
|- [_ x / x ]_ A = A
Theorem	csbeq1a 3147	Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
|- ( x = A -> B = [_ A / x ]_ B )
Theorem	csbco 3148*	Composition law for chained substitutions into a class. Use the weaker csbcow 3149 when possible. (Contributed by NM, 10-Nov-2005.) (New usage is discouraged.)
|- [_ A / y ]_ [_ y / x ]_ B = [_ A / x ]_ B
Theorem	csbcow 3149*	Composition law for chained substitutions into a class. Version of csbco 3148 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-Nov-2005.) (Revised by GG, 25-Aug-2024.)
|- [_ A / y ]_ [_ y / x ]_ B = [_ A / x ]_ B
Theorem	csbtt 3150	Substitution doesn't affect a constant B (in which x is not free). (Contributed by Mario Carneiro, 14-Oct-2016.)
|- ( ( A e. V /\ F/_ x B ) -> [_ A / x ]_ B = B )
Theorem	csbconstgf 3151	Substitution doesn't affect a constant B (in which x is not free). (Contributed by NM, 10-Nov-2005.)
|- F/_ x B   =>    |- ( A e. V -> [_ A / x ]_ B = B )
Theorem	csbconstg 3152*	Substitution doesn't affect a constant B (in which x is not free). csbconstgf 3151 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.)
|- ( A e. V -> [_ A / x ]_ B = B )
Theorem	sbcel12g 3153	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 3154	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 3155	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 3156	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 3157*	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 3158*	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 3159*	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 3160*	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 3161*	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	csbeq2 3162	Substituting into equivalent classes gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
|- ( A. x B = C -> [_ A / x ]_ B = [_ A / x ]_ C )
Theorem	csbeq2d 3163	Formula-building deduction for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- F/ x ph   &    |- ( ph -> B = C )   =>    |- ( ph -> [_ A / x ]_ B = [_ A / x ]_ C )
Theorem	csbeq2dv 3164*	Formula-building deduction 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 3165	Formula-building inference 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 3166	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 3167*	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 3168	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 3169	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/_ x [_ A / x ]_ B )
Theorem	nfcsb1 3170	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
|- F/_ x A   =>    |- F/_ x [_ A / x ]_ B
Theorem	nfcsb1v 3171*	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	nfsbcdw 3172*	Version of nfsbcd 3062 with a disjoint variable condition. (Contributed by NM, 23-Nov-2005.) (Revised by GG, 10-Jan-2024.)
|- F/ y ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x [. A / y ]. ps )
Theorem	nfsbcw 3173*	Bound-variable hypothesis builder for class substitution. Version of nfsbc 3063 with a disjoint variable condition, which in the future may make it possible to reduce axiom usage. (Contributed by NM, 7-Sep-2014.) (Revised by GG, 10-Jan-2024.)
|- F/_ x A   &    |- F/ x ph   =>    |- F/ x [. A / y ]. ph
Theorem	nfcsbd 3174	Deduction version of nfcsb 3176. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.)
|- F/ y ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x [_ A / y ]_ B )
Theorem	nfcsbw 3175*	Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3176 with a disjoint variable condition. (Contributed by Mario Carneiro, 12-Oct-2016.) (Revised by GG, 10-Jan-2024.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x [_ A / y ]_ B
Theorem	nfcsb 3176	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x [_ A / y ]_ B
Theorem	csbhypf 3177*	Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 2864 for class substitution version. (Contributed by NM, 19-Dec-2008.)
|- F/_ x A   &    |- F/_ x C   &    |- ( x = A -> B = C )   =>    |- ( y = A -> [_ y / x ]_ B = C )
Theorem	csbiebt 3178*	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3182.) (Contributed by NM, 11-Nov-2005.)
|- ( ( A e. V /\ F/_ x C ) -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )
Theorem	csbiedf 3179*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016.)
|- F/ x ph   &    |- ( ph -> F/_ x C )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x = A ) -> B = C )   =>    |- ( ph -> [_ A / x ]_ B = C )
Theorem	csbieb 3180*	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/_ x C   =>    |- ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C )
Theorem	csbiebg 3181*	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/_ x C   =>    |- ( A e. V -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )
Theorem	csbiegf 3182*	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/_ x C )   &    |- ( x = A -> B = C )   =>    |- ( A e. V -> [_ A / x ]_ B = C )
Theorem	csbief 3183*	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/_ x C   &    |- ( x = A -> B = C )   =>    |- [_ A / x ]_ B = C
Theorem	csbie 3184*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019.)
|- A e. _V   &    |- ( x = A -> B = C )   =>    |- [_ A / x ]_ B = C
Theorem	csbied 3185*	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 3186*	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 3187*	Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 3188). (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- A e. _V   &    |- B e. _V   =>    |- ( A. x A. y ( ( x = A /\ y = B ) -> C = D ) -> [_ A / x ]_ [_ B / y ]_ C = D )
Theorem	csbie2 3188*	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 3189*	Conversion of implicit substitution to explicit class substitution. This version of sbcie 3077 avoids a disjointness condition on x and 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 3190	Nest the composition of two substitutions. (Contributed by Mario Carneiro, 11-Nov-2016.)
|- ( ( A e. V /\ A. y F/ x ph ) -> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) )
Theorem	csbnestgf 3191	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/_ x C ) -> [_ A / x ]_ [_ B / y ]_ C = [_ [_ A / x ]_ B / y ]_ C )
Theorem	sbcnestg 3192*	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 3193*	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	csbnest1g 3194	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	csbidmg 3195*	Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.)
|- ( A e. V -> [_ A / x ]_ [_ A / x ]_ B = [_ A / x ]_ B )
Theorem	sbcco3g 3196*	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	csbco3g 3197*	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	rspcsbela 3198*	Special case related to rspsbc 3126. (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 3199*	Two ways of expressing " x is (effectively) not free in A." (Contributed by Mario Carneiro, 14-Oct-2016.)
|- ( F/_ x A <-> A. y A. z [_ y / x ]_ A = [_ z / x ]_ A )
Theorem	csbabg 3200*	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 } )