Theorem sbc2iedf

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Thierry Arnoux, 4-Jul-2023)

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

Proof

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