Metamath Proof Explorer


Theorem rbropapd

Description: Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017)

Ref Expression
Hypotheses rbropapd.1 φM=fp|fWpψ
rbropapd.2 f=Fp=Pψχ
Assertion rbropapd φFXPYFMPFWPχ

Proof

Step Hyp Ref Expression
1 rbropapd.1 φM=fp|fWpψ
2 rbropapd.2 f=Fp=Pψχ
3 df-br FMPFPM
4 1 eleq2d φFPMFPfp|fWpψ
5 3 4 bitrid φFMPFPfp|fWpψ
6 breq12 f=Fp=PfWpFWP
7 6 2 anbi12d f=Fp=PfWpψFWPχ
8 7 opelopabga FXPYFPfp|fWpψFWPχ
9 5 8 sylan9bb φFXPYFMPFWPχ
10 9 ex φFXPYFMPFWPχ