Metamath Proof Explorer


Theorem mptmpoopabovdOLD

Description: Obsolete version of mptmpoopabovd as of 13-Dec-2024. (Contributed by Alexander van der Vekens, 8-Nov-2017) (Revised by AV, 15-Jan-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses mptmpoopabbrdOLD.g φ G W
mptmpoopabbrdOLD.x φ X A G
mptmpoopabbrdOLD.y φ Y B G
mptmpoopabbrdOLD.v φ f h | ψ V
mptmpoopabbrdOLD.r φ f D G h ψ
mptmpoopabovdOLD.m M = g V a A g , b B g f h | f a C g b h f D g h
Assertion mptmpoopabovdOLD φ X M G Y = f h | f X C G Y h f D G h

Proof

Step Hyp Ref Expression
1 mptmpoopabbrdOLD.g φ G W
2 mptmpoopabbrdOLD.x φ X A G
3 mptmpoopabbrdOLD.y φ Y B G
4 mptmpoopabbrdOLD.v φ f h | ψ V
5 mptmpoopabbrdOLD.r φ f D G h ψ
6 mptmpoopabovdOLD.m M = g V a A g , b B g f h | f a C g b h f D g h
7 oveq12 a = X b = Y a C G b = X C G Y
8 7 breqd a = X b = Y f a C G b h f X C G Y h
9 fveq2 g = G C g = C G
10 9 oveqd g = G a C g b = a C G b
11 10 breqd g = G f a C g b h f a C G b h
12 1 2 3 4 5 8 11 6 mptmpoopabbrdOLD φ X M G Y = f h | f X C G Y h f D G h