Theorem sbc2iegf

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Dec-2013)

	Ref	Expression
Hypotheses	sbc2iegf.1	|- F/ x ps
	sbc2iegf.2	|- F/ y ps
	sbc2iegf.3	|- F/ x B e. W
	sbc2iegf.4	|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
Assertion	sbc2iegf	|- ( ( A e. V /\ B e. W ) -> ( [. A / x ]. [. B / y ]. ph <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		sbc2iegf.1	|- F/ x ps
2		sbc2iegf.2	|- F/ y ps
3		sbc2iegf.3	|- F/ x B e. W
4		sbc2iegf.4	|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
5		simpl	|- ( ( A e. V /\ B e. W ) -> A e. V )
6		simpl	|- ( ( B e. W /\ x = A ) -> B e. W )
7	4	adantll	|- ( ( ( B e. W /\ x = A ) /\ y = B ) -> ( ph <-> ps ) )
8		nfv	|- F/ y ( B e. W /\ x = A )
9	2	a1i	|- ( ( B e. W /\ x = A ) -> F/ y ps )
10	6 7 8 9	sbciedf	|- ( ( B e. W /\ x = A ) -> ( [. B / y ]. ph <-> ps ) )
11	10	adantll	|- ( ( ( A e. V /\ B e. W ) /\ x = A ) -> ( [. B / y ]. ph <-> ps ) )
12		nfv	|- F/ x A e. V
13	12 3	nfan	|- F/ x ( A e. V /\ B e. W )
14	1	a1i	|- ( ( A e. V /\ B e. W ) -> F/ x ps )
15	5 11 13 14	sbciedf	|- ( ( A e. V /\ B e. W ) -> ( [. A / x ]. [. B / y ]. ph <-> ps ) )