Metamath Proof Explorer


Theorem bj-dfmpoa

Description: An equivalent definition of df-mpo . (Contributed by BJ, 30-Dec-2020)

Ref Expression
Assertion bj-dfmpoa xA,yBC=st|xAyBs=xyt=C

Proof

Step Hyp Ref Expression
1 df-mpo xA,yBC=xyt|xAyBt=C
2 dfoprab2 xyt|xAyBt=C=st|xys=xyxAyBt=C
3 ancom xAyBt=Ct=CxAyB
4 3 anbi2i s=xyxAyBt=Cs=xyt=CxAyB
5 anass s=xyt=CxAyBs=xyt=CxAyB
6 an13 s=xyt=CxAyByBxAs=xyt=C
7 4 5 6 3bitr2i s=xyxAyBt=CyBxAs=xyt=C
8 7 exbii ys=xyxAyBt=CyyBxAs=xyt=C
9 df-rex yBxAs=xyt=CyyBxAs=xyt=C
10 r19.42v yBxAs=xyt=CxAyBs=xyt=C
11 8 9 10 3bitr2i ys=xyxAyBt=CxAyBs=xyt=C
12 11 exbii xys=xyxAyBt=CxxAyBs=xyt=C
13 df-rex xAyBs=xyt=CxxAyBs=xyt=C
14 12 13 bitr4i xys=xyxAyBt=CxAyBs=xyt=C
15 14 opabbii st|xys=xyxAyBt=C=st|xAyBs=xyt=C
16 1 2 15 3eqtri xA,yBC=st|xAyBs=xyt=C