Metamath Proof Explorer


Theorem resoprab

Description: Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007)

Ref Expression
Assertion resoprab x y z | φ A × B = x y z | x A y B φ

Proof

Step Hyp Ref Expression
1 resopab w z | x y w = x y φ A × B = w z | w A × B x y w = x y φ
2 19.42vv x y w A × B w = x y φ w A × B x y w = x y φ
3 an12 w A × B w = x y φ w = x y w A × B φ
4 eleq1 w = x y w A × B x y A × B
5 opelxp x y A × B x A y B
6 4 5 bitrdi w = x y w A × B x A y B
7 6 anbi1d w = x y w A × B φ x A y B φ
8 7 pm5.32i w = x y w A × B φ w = x y x A y B φ
9 3 8 bitri w A × B w = x y φ w = x y x A y B φ
10 9 2exbii x y w A × B w = x y φ x y w = x y x A y B φ
11 2 10 bitr3i w A × B x y w = x y φ x y w = x y x A y B φ
12 11 opabbii w z | w A × B x y w = x y φ = w z | x y w = x y x A y B φ
13 1 12 eqtri w z | x y w = x y φ A × B = w z | x y w = x y x A y B φ
14 dfoprab2 x y z | φ = w z | x y w = x y φ
15 14 reseq1i x y z | φ A × B = w z | x y w = x y φ A × B
16 dfoprab2 x y z | x A y B φ = w z | x y w = x y x A y B φ
17 13 15 16 3eqtr4i x y z | φ A × B = x y z | x A y B φ