P. 29 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2801-2900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elrabsf 2801	Membership in a restricted class abstraction, expressed with explicit class substitution. (The variation elrabf 2696 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	eqsbc3 2802*	Substitution applied to an atomic wff. Set theory version of eqsb3 2141. (Contributed by Andrew Salmon, 29-Jun-2011.)
|- ( A e. V -> ( [. A / x ]. x = B <-> A = B ) )
Theorem	sbcng 2803	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 2804	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 2805	Distribution of class substitution over conjunction. (Contributed by NM, 31-Dec-2016.)
|- ( [. A / x ]. ( ph /\ ps ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps ) )
Theorem	sbcang 2806	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 2807	Distribution of class substitution over disjunction. (Contributed by NM, 31-Dec-2016.)
|- ( [. A / x ]. ( ph \/ ps ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps ) )
Theorem	sbcorg 2808	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 2809	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	sbcal 2810*	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 2811*	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 2812*	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 2813*	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 2814*	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 2815*	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 2816	Formula-building deduction rule for class substitution. (Contributed by NM, 29-Dec-2014.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( [. A / x ]. ps <-> [. A / x ]. ch ) )
Theorem	sbcbidv 2817*	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 2818	Formula-building inference rule for class substitution. (Contributed by NM, 11-Nov-2005.)
|- ( ph <-> ps )   =>    |- ( [. A / x ]. ph <-> [. A / x ]. ps )
Theorem	eqsbc3r 2819*	eqsbc3 2802 with setvar variable on right side of equals sign. (Contributed by Alan Sare, 24-Oct-2011.)
|- ( A e. B -> ( [. A / x ]. C = x <-> C = A ) )
Theorem	sbc3ang 2820	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 2821*	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 2822*	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 2823*	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 2824	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 2825	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 2826	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 2827*	Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 2825. (Contributed by Alan Sare, 10-Nov-2012.)
|- ( A e. V -> ( [. A / x ]. ph <-> ph ) )
Theorem	sbc2iegf 2828*	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 2829*	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 2830*	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 2831*	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 2832*	Lemma for sbccom 2833. (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 2833*	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 2834*	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 2835*	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 2836*	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 2837*	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 2838*	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 2839*	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 2840*	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 1658 and spsbc 2775. See also rspsbca 2841 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 2841*	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 2842*	Existence form of rspsbca 2841. (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 2843	Existence form of spsbc 2775. (Contributed by Mario Carneiro, 18-Nov-2016.)
|- ( [. A / x ]. ph -> E. x ph )
Theorem	spesbcd 2844	form of spsbc 2775. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ph -> [. A / x ]. ps )   =>    |- ( ph -> E. x ps )
Theorem	sbcth2 2845*	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 2846	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 1476. (Contributed by NM, 16-Jan-2004.)
|- F/ x ph   =>    |- ( A. x e. A ( ph -> ps ) -> ( ph -> A. x e. A ps ) )
Theorem	rmo2ilem 2847*	Condition implying restricted "at most one." (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 2848*	Condition implying restricted "at most one." (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 2849*	Restricted "at most one" 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 2850*	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 2851*	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 2852	Extend class notation to include the proper substitution of a class for a set into another class.
class [_ A / x ]_ B
Definition	df-csb 2853*	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 2764, to prevent ambiguity. Theorem sbcel1g 2869 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2878 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 2854*	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 2855	Analog of dfsbcq 2766 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
|- ( A = B -> [_ A / x ]_ C = [_ B / x ]_ C )
Theorem	cbvcsb 2856	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 2857*	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 2858	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 2859	Analog of sbid 1657 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
|- [_ x / x ]_ A = A
Theorem	csbeq1a 2860	Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
|- ( x = A -> B = [_ A / x ]_ B )
Theorem	csbco 2861*	Composition law for chained substitutions into a class. (Contributed by NM, 10-Nov-2005.)
|- [_ A / y ]_ [_ y / x ]_ B = [_ A / x ]_ B
Theorem	csbtt 2862	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 2863	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 2864*	Substitution doesn't affect a constant B (in which x is not free). csbconstgf 2863 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.)
|- ( A e. V -> [_ A / x ]_ B = B )
Theorem	sbcel12g 2865	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 2866	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 2867	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 2868	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 2869*	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 2870*	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 2871*	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 2872*	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 2873*	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 2874	Formula-building deduction rule 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 2875*	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 2876	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 2877	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 2878*	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 2879	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 2880	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 2881	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 2882*	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 2883	Deduction version of nfcsb 2884. (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	nfcsb 2884	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 2885*	Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 2603 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 2886*	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 2890.) (Contributed by NM, 11-Nov-2005.)
|- ( ( A e. V /\ F/_ x C ) -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )
Theorem	csbiedf 2887*	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 2888*	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 2889*	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 2890*	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 2891*	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	csbied 2892*	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 2893*	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 2894*	Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 2895). (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 2895*	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 2896*	Conversion of implicit substitution to explicit class substitution. This version of sbcie 2797 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 2897	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 2898	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 2899*	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 2900*	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 )