Metamath Proof Explorer


Theorem rabxp

Description: Class abstraction restricted to a Cartesian product as an ordered-pair class abstraction. (Contributed by NM, 20-Feb-2014)

Ref Expression
Hypothesis rabxp.1 x=yzφψ
Assertion rabxp xA×B|φ=yz|yAzBψ

Proof

Step Hyp Ref Expression
1 rabxp.1 x=yzφψ
2 elxp xA×Byzx=yzyAzB
3 2 anbi1i xA×Bφyzx=yzyAzBφ
4 19.41vv yzx=yzyAzBφyzx=yzyAzBφ
5 anass x=yzyAzBφx=yzyAzBφ
6 1 anbi2d x=yzyAzBφyAzBψ
7 df-3an yAzBψyAzBψ
8 6 7 bitr4di x=yzyAzBφyAzBψ
9 8 pm5.32i x=yzyAzBφx=yzyAzBψ
10 5 9 bitri x=yzyAzBφx=yzyAzBψ
11 10 2exbii yzx=yzyAzBφyzx=yzyAzBψ
12 3 4 11 3bitr2i xA×Bφyzx=yzyAzBψ
13 12 abbii x|xA×Bφ=x|yzx=yzyAzBψ
14 df-rab xA×B|φ=x|xA×Bφ
15 df-opab yz|yAzBψ=x|yzx=yzyAzBψ
16 13 14 15 3eqtr4i xA×B|φ=yz|yAzBψ