Theorem vtocl2dOLD

Description: Obsolete version of vtocl2d as of 19-Oct-2023. (Contributed by Thierry Arnoux, 25-Aug-2020) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	vtocl2dOLD.a	|- ( ph -> A e. V )
	vtocl2dOLD.b	|- ( ph -> B e. W )
	vtocl2dOLD.1	|- ( ( x = A /\ y = B ) -> ( ps <-> ch ) )
	vtocl2dOLD.3	|- ( ph -> ps )
Assertion	vtocl2dOLD	|- ( ph -> ch )

Proof

Step	Hyp	Ref	Expression
1		vtocl2dOLD.a	|- ( ph -> A e. V )
2		vtocl2dOLD.b	|- ( ph -> B e. W )
3		vtocl2dOLD.1	|- ( ( x = A /\ y = B ) -> ( ps <-> ch ) )
4		vtocl2dOLD.3	|- ( ph -> ps )
5		nfcv	|- F/_ y B
6		nfcv	|- F/_ x B
7		nfcv	|- F/_ x A
8		nfv	|- F/ y ph
9		nfsbc1v	|- F/ y [. B / y ]. ps
10	8 9	nfim	|- F/ y ( ph -> [. B / y ]. ps )
11		nfv	|- F/ x ( ph -> ch )
12		sbceq1a	|- ( y = B -> ( ps <-> [. B / y ]. ps ) )
13	12	imbi2d	|- ( y = B -> ( ( ph -> ps ) <-> ( ph -> [. B / y ]. ps ) ) )
14		sbceq1a	|- ( x = A -> ( [. B / y ]. ps <-> [. A / x ]. [. B / y ]. ps ) )
15		nfv	|- F/ x ch
16		nfv	|- F/ y ch
17		nfv	|- F/ x B e. W
18	15 16 17 3	sbc2iegf	|- ( ( A e. V /\ B e. W ) -> ( [. A / x ]. [. B / y ]. ps <-> ch ) )
19	1 2 18	syl2anc	|- ( ph -> ( [. A / x ]. [. B / y ]. ps <-> ch ) )
20	14 19	sylan9bb	|- ( ( x = A /\ ph ) -> ( [. B / y ]. ps <-> ch ) )
21	20	pm5.74da	|- ( x = A -> ( ( ph -> [. B / y ]. ps ) <-> ( ph -> ch ) ) )
22	5 6 7 10 11 13 21 4	vtocl2gf	|- ( ( B e. W /\ A e. V ) -> ( ph -> ch ) )
23	2 1 22	syl2anc	|- ( ph -> ( ph -> ch ) )
24	23	pm2.43i	|- ( ph -> ch )