Metamath Proof Explorer


Theorem csboprabg

Description: Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020)

Ref Expression
Assertion csboprabg AVA/xyzd|φ=yzd|[˙A/x]˙φ

Proof

Step Hyp Ref Expression
1 csbab A/xc|yzdc=yzdφ=c|[˙A/x]˙yzdc=yzdφ
2 sbcex2 [˙A/x]˙yzdc=yzdφy[˙A/x]˙zdc=yzdφ
3 sbcex2 [˙A/x]˙zdc=yzdφz[˙A/x]˙dc=yzdφ
4 sbcex2 [˙A/x]˙dc=yzdφd[˙A/x]˙c=yzdφ
5 sbcan [˙A/x]˙c=yzdφ[˙A/x]˙c=yzd[˙A/x]˙φ
6 sbcg AV[˙A/x]˙c=yzdc=yzd
7 6 anbi1d AV[˙A/x]˙c=yzd[˙A/x]˙φc=yzd[˙A/x]˙φ
8 5 7 syl5bb AV[˙A/x]˙c=yzdφc=yzd[˙A/x]˙φ
9 8 exbidv AVd[˙A/x]˙c=yzdφdc=yzd[˙A/x]˙φ
10 4 9 syl5bb AV[˙A/x]˙dc=yzdφdc=yzd[˙A/x]˙φ
11 10 exbidv AVz[˙A/x]˙dc=yzdφzdc=yzd[˙A/x]˙φ
12 3 11 syl5bb AV[˙A/x]˙zdc=yzdφzdc=yzd[˙A/x]˙φ
13 12 exbidv AVy[˙A/x]˙zdc=yzdφyzdc=yzd[˙A/x]˙φ
14 2 13 syl5bb AV[˙A/x]˙yzdc=yzdφyzdc=yzd[˙A/x]˙φ
15 14 abbidv AVc|[˙A/x]˙yzdc=yzdφ=c|yzdc=yzd[˙A/x]˙φ
16 1 15 eqtrid AVA/xc|yzdc=yzdφ=c|yzdc=yzd[˙A/x]˙φ
17 df-oprab yzd|φ=c|yzdc=yzdφ
18 17 csbeq2i A/xyzd|φ=A/xc|yzdc=yzdφ
19 df-oprab yzd|[˙A/x]˙φ=c|yzdc=yzd[˙A/x]˙φ
20 16 18 19 3eqtr4g AVA/xyzd|φ=yzd|[˙A/x]˙φ