Metamath Proof Explorer


Theorem fmptcof

Description: Version of fmptco where ph needn't be distinct from x . (Contributed by NM, 27-Dec-2014)

Ref Expression
Hypotheses fmptcof.1 φ x A R B
fmptcof.2 φ F = x A R
fmptcof.3 φ G = y B S
fmptcof.4 y = R S = T
Assertion fmptcof φ G F = x A T

Proof

Step Hyp Ref Expression
1 fmptcof.1 φ x A R B
2 fmptcof.2 φ F = x A R
3 fmptcof.3 φ G = y B S
4 fmptcof.4 y = R S = T
5 nfcsb1v _ x z / x R
6 5 nfel1 x z / x R B
7 csbeq1a x = z R = z / x R
8 7 eleq1d x = z R B z / x R B
9 6 8 rspc z A x A R B z / x R B
10 1 9 mpan9 φ z A z / x R B
11 nfcv _ z R
12 11 5 7 cbvmpt x A R = z A z / x R
13 2 12 eqtrdi φ F = z A z / x R
14 nfcv _ w S
15 nfcsb1v _ y w / y S
16 csbeq1a y = w S = w / y S
17 14 15 16 cbvmpt y B S = w B w / y S
18 3 17 eqtrdi φ G = w B w / y S
19 csbeq1 w = z / x R w / y S = z / x R / y S
20 10 13 18 19 fmptco φ G F = z A z / x R / y S
21 nfcv _ z R / y S
22 nfcv _ x S
23 5 22 nfcsbw _ x z / x R / y S
24 7 csbeq1d x = z R / y S = z / x R / y S
25 21 23 24 cbvmpt x A R / y S = z A z / x R / y S
26 20 25 eqtr4di φ G F = x A R / y S
27 eqid A = A
28 nfcvd R B _ y T
29 28 4 csbiegf R B R / y S = T
30 29 ralimi x A R B x A R / y S = T
31 mpteq12 A = A x A R / y S = T x A R / y S = x A T
32 27 30 31 sylancr x A R B x A R / y S = x A T
33 1 32 syl φ x A R / y S = x A T
34 26 33 eqtrd φ G F = x A T