Metamath Proof Explorer


Theorem mulc1cncfg

Description: A version of mulc1cncf using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 30-Jun-2017)

Ref Expression
Hypotheses mulc1cncfg.1 _xF
mulc1cncfg.2 xφ
mulc1cncfg.3 φF:Acn
mulc1cncfg.4 φB
Assertion mulc1cncfg φxABFx:Acn

Proof

Step Hyp Ref Expression
1 mulc1cncfg.1 _xF
2 mulc1cncfg.2 xφ
3 mulc1cncfg.3 φF:Acn
4 mulc1cncfg.4 φB
5 eqid xBx=xBx
6 5 mulc1cncf BxBx:cn
7 4 6 syl φxBx:cn
8 cncff xBx:cnxBx:
9 7 8 syl φxBx:
10 cncff F:AcnF:A
11 3 10 syl φF:A
12 fcompt xBx:F:AxBxF=tAxBxFt
13 9 11 12 syl2anc φxBxF=tAxBxFt
14 11 ffvelrnda φtAFt
15 4 adantr φtAB
16 15 14 mulcld φtABFt
17 nfcv _xt
18 1 17 nffv _xFt
19 nfcv _xB
20 nfcv _x×
21 19 20 18 nfov _xBFt
22 oveq2 x=FtBx=BFt
23 18 21 22 5 fvmptf FtBFtxBxFt=BFt
24 14 16 23 syl2anc φtAxBxFt=BFt
25 24 mpteq2dva φtAxBxFt=tABFt
26 nfcv _tB
27 nfcv _t×
28 nfcv _tFx
29 26 27 28 nfov _tBFx
30 fveq2 t=xFt=Fx
31 30 oveq2d t=xBFt=BFx
32 21 29 31 cbvmpt tABFt=xABFx
33 25 32 eqtrdi φtAxBxFt=xABFx
34 13 33 eqtrd φxBxF=xABFx
35 3 7 cncfco φxBxF:Acn
36 34 35 eqeltrrd φxABFx:Acn