P. 31 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3001-3100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfsbcd 3001	Deduction version of nfsbc 3002. (Contributed by NM, 23-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.)
|- F/ y ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x [. A / y ]. ps )
Theorem	nfsbc 3002	Bound-variable hypothesis builder for class substitution. (Contributed by NM, 7-Sep-2014.) (Revised by Mario Carneiro, 12-Oct-2016.)
|- F/_ x A   &    |- F/ x ph   =>    |- F/ x [. A / y ]. ph
Theorem	sbcco 3003*	A composition law for class substitution. (Contributed by NM, 26-Sep-2003.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph )
Theorem	sbcco2 3004*	A composition law for class substitution. Importantly, x may occur free in the class expression substituted for A. (Contributed by NM, 5-Sep-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|- ( x = y -> A = B )   =>    |- ( [. x / y ]. [. B / x ]. ph <-> [. A / x ]. ph )
Theorem	sbc5 3005*	An equivalence for class substitution. (Contributed by NM, 23-Aug-1993.) (Revised by Mario Carneiro, 12-Oct-2016.)
|- ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) )
Theorem	sbc6g 3006*	An equivalence for class substitution. (Contributed by NM, 11-Oct-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|- ( A e. V -> ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) )
Theorem	sbc6 3007*	An equivalence for class substitution. (Contributed by NM, 23-Aug-1993.) (Proof shortened by Eric Schmidt, 17-Jan-2007.)
|- A e. _V   =>    |- ( [. A / x ]. ph <-> A. x ( x = A -> ph ) )
Theorem	sbc7 3008*	An equivalence for class substitution in the spirit of df-clab 2176. Note that x and A don't have to be distinct. (Contributed by NM, 18-Nov-2008.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- ( [. A / x ]. ph <-> E. y ( y = A /\ [. y / x ]. ph ) )
Theorem	cbvsbcw 3009*	Version of cbvsbc 3010 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( [. A / x ]. ph <-> [. A / y ]. ps )
Theorem	cbvsbc 3010	Change bound variables in a wff substitution. (Contributed by Jeff Hankins, 19-Sep-2009.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( [. A / x ]. ph <-> [. A / y ]. ps )
Theorem	cbvsbcv 3011*	Change the bound variable of a class substitution using implicit substitution. (Contributed by NM, 30-Sep-2008.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( [. A / x ]. ph <-> [. A / y ]. ps )
Theorem	sbciegft 3012*	Conversion of implicit substitution to explicit class substitution, using a bound-variable hypothesis instead of distinct variables. (Closed theorem version of sbciegf 3013.) (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- ( ( A e. V /\ F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( [. A / x ]. ph <-> ps ) )
Theorem	sbciegf 3013*	Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- F/ x ps   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( [. A / x ]. ph <-> ps ) )
Theorem	sbcieg 3014*	Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( [. A / x ]. ph <-> ps ) )
Theorem	sbcie2g 3015*	Conversion of implicit substitution to explicit class substitution. This version of sbcie 3016 avoids a disjointness condition on x and A by substituting twice. (Contributed by Mario Carneiro, 15-Oct-2016.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( y = A -> ( ps <-> ch ) )   =>    |- ( A e. V -> ( [. A / x ]. ph <-> ch ) )
Theorem	sbcie 3016*	Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004.)
|- A e. _V   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( [. A / x ]. ph <-> ps )
Theorem	sbciedf 3017*	Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 29-Dec-2014.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   &    |- F/ x ph   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> ( [. A / x ]. ps <-> ch ) )
Theorem	sbcied 3018*	Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( [. A / x ]. ps <-> ch ) )
Theorem	sbcied2 3019*	Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> A = B )   &    |- ( ( ph /\ x = B ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( [. A / x ]. ps <-> ch ) )
Theorem	elrabsf 3020	Membership in a restricted class abstraction, expressed with explicit class substitution. (The variation elrabf 2910 has implicit substitution). The hypothesis specifies that x must not be a free variable in B. (Contributed by NM, 30-Sep-2003.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
|- F/_ x B   =>    |- ( A e. { x e. B | ph } <-> ( A e. B /\ [. A / x ]. ph ) )
Theorem	eqsbc1 3021*	Substitution for the left-hand side in an equality. Class version of eqsb1 2293. (Contributed by Andrew Salmon, 29-Jun-2011.)
|- ( A e. V -> ( [. A / x ]. x = B <-> A = B ) )
Theorem	sbcng 3022	Move negation in and out of class substitution. (Contributed by NM, 16-Jan-2004.)
|- ( A e. V -> ( [. A / x ]. -. ph <-> -. [. A / x ]. ph ) )
Theorem	sbcimg 3023	Distribution of class substitution over implication. (Contributed by NM, 16-Jan-2004.)
|- ( A e. V -> ( [. A / x ]. ( ph -> ps ) <-> ( [. A / x ]. ph -> [. A / x ]. ps ) ) )
Theorem	sbcan 3024	Distribution of class substitution over conjunction. (Contributed by NM, 31-Dec-2016.)
|- ( [. A / x ]. ( ph /\ ps ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps ) )
Theorem	sbcang 3025	Distribution of class substitution over conjunction. (Contributed by NM, 21-May-2004.)
|- ( A e. V -> ( [. A / x ]. ( ph /\ ps ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps ) ) )
Theorem	sbcor 3026	Distribution of class substitution over disjunction. (Contributed by NM, 31-Dec-2016.)
|- ( [. A / x ]. ( ph \/ ps ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps ) )
Theorem	sbcorg 3027	Distribution of class substitution over disjunction. (Contributed by NM, 21-May-2004.)
|- ( A e. V -> ( [. A / x ]. ( ph \/ ps ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps ) ) )
Theorem	sbcbig 3028	Distribution of class substitution over biconditional. (Contributed by Raph Levien, 10-Apr-2004.)
|- ( A e. V -> ( [. A / x ]. ( ph <-> ps ) <-> ( [. A / x ]. ph <-> [. A / x ]. ps ) ) )
Theorem	sbcn1 3029	Move negation in and out of class substitution. One direction of sbcng 3022 that holds for proper classes. (Contributed by NM, 17-Aug-2018.)
|- ( [. A / x ]. -. ph -> -. [. A / x ]. ph )
Theorem	sbcim1 3030	Distribution of class substitution over implication. One direction of sbcimg 3023 that holds for proper classes. (Contributed by NM, 17-Aug-2018.)
|- ( [. A / x ]. ( ph -> ps ) -> ( [. A / x ]. ph -> [. A / x ]. ps ) )
Theorem	sbcbi1 3031	Distribution of class substitution over biconditional. One direction of sbcbig 3028 that holds for proper classes. (Contributed by NM, 17-Aug-2018.)
|- ( [. A / x ]. ( ph <-> ps ) -> ( [. A / x ]. ph <-> [. A / x ]. ps ) )
Theorem	sbcbi2 3032	Substituting into equivalent wff's gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
|- ( A. x ( ph <-> ps ) -> ( [. A / x ]. ph <-> [. A / x ]. ps ) )
Theorem	sbcal 3033*	Move universal quantifier in and out of class substitution. (Contributed by NM, 31-Dec-2016.)
|- ( [. A / y ]. A. x ph <-> A. x [. A / y ]. ph )
Theorem	sbcalg 3034*	Move universal quantifier in and out of class substitution. (Contributed by NM, 16-Jan-2004.)
|- ( A e. V -> ( [. A / y ]. A. x ph <-> A. x [. A / y ]. ph ) )
Theorem	sbcex2 3035*	Move existential quantifier in and out of class substitution. (Contributed by NM, 21-May-2004.)
|- ( [. A / y ]. E. x ph <-> E. x [. A / y ]. ph )
Theorem	sbcexg 3036*	Move existential quantifier in and out of class substitution. (Contributed by NM, 21-May-2004.)
|- ( A e. V -> ( [. A / y ]. E. x ph <-> E. x [. A / y ]. ph ) )
Theorem	sbceqal 3037*	A variation of extensionality for classes. (Contributed by Andrew Salmon, 28-Jun-2011.)
|- ( A e. V -> ( A. x ( x = A -> x = B ) -> A = B ) )
Theorem	sbeqalb 3038*	Theorem *14.121 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 28-Jun-2011.) (Proof shortened by Wolf Lammen, 9-May-2013.)
|- ( A e. V -> ( ( A. x ( ph <-> x = A ) /\ A. x ( ph <-> x = B ) ) -> A = B ) )
Theorem	sbcbid 3039	Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( [. A / x ]. ps <-> [. A / x ]. ch ) )
Theorem	sbcbidv 3040*	Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( [. A / x ]. ps <-> [. A / x ]. ch ) )
Theorem	sbcbii 3041	Formula-building inference for class substitution. (Contributed by NM, 11-Nov-2005.)
|- ( ph <-> ps )   =>    |- ( [. A / x ]. ph <-> [. A / x ]. ps )
Theorem	eqsbc2 3042*	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 3043	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 3044*	Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.)
|- ( [. A / x ]. x e. B <-> A e. B )
Theorem	sbcel2gv 3045*	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 3046*	Class substitution into a membership relation. One direction of sbcel2gv 3045 that holds for proper classes. (Contributed by NM, 17-Aug-2018.)
|- ( [. B / x ]. A e. x -> A e. B )
Theorem	sbcimdv 3047*	Substitution analogue of Theorem 19.20 of [Margaris] p. 90 (alim 1468). (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 3048	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 3049	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 3050	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 3051*	Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3049. (Contributed by Alan Sare, 10-Nov-2012.)
|- ( A e. V -> ( [. A / x ]. ph <-> ph ) )
Theorem	sbc2iegf 3052*	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 3053*	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 3054*	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 3055*	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 3056*	Lemma for sbccom 3057. (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 3057*	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 3058*	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 3059*	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 3060*	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 3061*	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 3062*	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	sbcabel 3063*	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 3064*	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 1786 and spsbc 2993. See also rspsbca 3065 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 3065*	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 3066*	Existence form of rspsbca 3065. (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 3067	Existence form of spsbc 2993. (Contributed by Mario Carneiro, 18-Nov-2016.)
|- ( [. A / x ]. ph -> E. x ph )
Theorem	spesbcd 3068	form of spsbc 2993. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ph -> [. A / x ]. ps )   =>    |- ( ph -> E. x ps )
Theorem	sbcth2 3069*	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 3070	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 1595. (Contributed by NM, 16-Jan-2004.)
|- F/ x ph   =>    |- ( A. x e. A ( ph -> ps ) -> ( ph -> A. x e. A ps ) )
Theorem	rmo2ilem 3071*	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 3072*	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 3073*	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 3074*	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 3075*	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 3076	Extend class notation to include the proper substitution of a class for a set into another class.
class [_ A / x ]_ B
Definition	df-csb 3077*	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 2981, to prevent ambiguity. Theorem sbcel1g 3095 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3105 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 3078*	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 3079	Analog of dfsbcq 2983 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
|- ( A = B -> [_ A / x ]_ C = [_ B / x ]_ C )
Theorem	cbvcsbw 3080*	Version of cbvcsb 3081 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 3081	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 3082*	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 3083	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 3084	Analog of sbid 1785 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
|- [_ x / x ]_ A = A
Theorem	csbeq1a 3085	Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
|- ( x = A -> B = [_ A / x ]_ B )
Theorem	csbco 3086*	Composition law for chained substitutions into a class. Use the weaker csbcow 3087 when possible. (Contributed by NM, 10-Nov-2005.) (New usage is discouraged.)
|- [_ A / y ]_ [_ y / x ]_ B = [_ A / x ]_ B
Theorem	csbcow 3087*	Composition law for chained substitutions into a class. Version of csbco 3086 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 3088	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 3089	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 3090*	Substitution doesn't affect a constant B (in which x is not free). csbconstgf 3089 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.)
|- ( A e. V -> [_ A / x ]_ B = B )
Theorem	sbcel12g 3091	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 3092	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 3093	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 3094	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 3095*	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 3096*	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 3097*	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 3098*	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 3099*	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 3100	Substituting into equivalent classes gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
|- ( A. x B = C -> [_ A / x ]_ B = [_ A / x ]_ C )