Metamath Proof Explorer


Theorem cbvmpo2

Description: Rule to change the second bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses cbvmpo2.1 _yA
cbvmpo2.2 _wA
cbvmpo2.3 _wC
cbvmpo2.4 _yE
cbvmpo2.5 y=wC=E
Assertion cbvmpo2 xA,yBC=xA,wBE

Proof

Step Hyp Ref Expression
1 cbvmpo2.1 _yA
2 cbvmpo2.2 _wA
3 cbvmpo2.3 _wC
4 cbvmpo2.4 _yE
5 cbvmpo2.5 y=wC=E
6 2 nfcri wxA
7 nfcv _wB
8 7 nfcri wyB
9 6 8 nfan wxAyB
10 3 nfeq2 wu=C
11 9 10 nfan wxAyBu=C
12 1 nfcri yxA
13 nfv ywB
14 12 13 nfan yxAwB
15 4 nfeq2 yu=E
16 14 15 nfan yxAwBu=E
17 eleq1w y=wyBwB
18 17 anbi2d y=wxAyBxAwB
19 5 eqeq2d y=wu=Cu=E
20 18 19 anbi12d y=wxAyBu=CxAwBu=E
21 11 16 20 cbvoprab2 xyu|xAyBu=C=xwu|xAwBu=E
22 df-mpo xA,yBC=xyu|xAyBu=C
23 df-mpo xA,wBE=xwu|xAwBu=E
24 21 22 23 3eqtr4i xA,yBC=xA,wBE