Metamath Proof Explorer


Theorem csbmpo123

Description: Move class substitution in and out of maps-to notation for operations. (Contributed by ML, 25-Oct-2020)

Ref Expression
Assertion csbmpo123 A V A / x y Y , z Z D = y A / x Y , z A / x Z A / x D

Proof

Step Hyp Ref Expression
1 csboprabg A V A / x y z d | y Y z Z d = D = y z d | [˙A / x]˙ y Y z Z d = D
2 sbcan [˙A / x]˙ y Y z Z d = D [˙A / x]˙ y Y z Z [˙A / x]˙ d = D
3 sbcan [˙A / x]˙ y Y z Z [˙A / x]˙ y Y [˙A / x]˙ z Z
4 sbcel12 [˙A / x]˙ y Y A / x y A / x Y
5 csbconstg A V A / x y = y
6 5 eleq1d A V A / x y A / x Y y A / x Y
7 4 6 syl5bb A V [˙A / x]˙ y Y y A / x Y
8 sbcel12 [˙A / x]˙ z Z A / x z A / x Z
9 csbconstg A V A / x z = z
10 9 eleq1d A V A / x z A / x Z z A / x Z
11 8 10 syl5bb A V [˙A / x]˙ z Z z A / x Z
12 7 11 anbi12d A V [˙A / x]˙ y Y [˙A / x]˙ z Z y A / x Y z A / x Z
13 3 12 syl5bb A V [˙A / x]˙ y Y z Z y A / x Y z A / x Z
14 sbceq2g A V [˙A / x]˙ d = D d = A / x D
15 13 14 anbi12d A V [˙A / x]˙ y Y z Z [˙A / x]˙ d = D y A / x Y z A / x Z d = A / x D
16 2 15 syl5bb A V [˙A / x]˙ y Y z Z d = D y A / x Y z A / x Z d = A / x D
17 16 oprabbidv A V y z d | [˙A / x]˙ y Y z Z d = D = y z d | y A / x Y z A / x Z d = A / x D
18 1 17 eqtrd A V A / x y z d | y Y z Z d = D = y z d | y A / x Y z A / x Z d = A / x D
19 df-mpo y Y , z Z D = y z d | y Y z Z d = D
20 19 csbeq2i A / x y Y , z Z D = A / x y z d | y Y z Z d = D
21 df-mpo y A / x Y , z A / x Z A / x D = y z d | y A / x Y z A / x Z d = A / x D
22 18 20 21 3eqtr4g A V A / x y Y , z Z D = y A / x Y , z A / x Z A / x D