Metamath Proof Explorer


Theorem opabbid

Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 21-Feb-2004) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Hypotheses opabbid.1 xφ
opabbid.2 yφ
opabbid.3 φψχ
Assertion opabbid φxy|ψ=xy|χ

Proof

Step Hyp Ref Expression
1 opabbid.1 xφ
2 opabbid.2 yφ
3 opabbid.3 φψχ
4 3 anbi2d φz=xyψz=xyχ
5 2 4 exbid φyz=xyψyz=xyχ
6 1 5 exbid φxyz=xyψxyz=xyχ
7 6 abbidv φz|xyz=xyψ=z|xyz=xyχ
8 df-opab xy|ψ=z|xyz=xyψ
9 df-opab xy|χ=z|xyz=xyχ
10 7 8 9 3eqtr4g φxy|ψ=xy|χ