Metamath Proof Explorer


Theorem xpab

Description: Cross product of two class abstractions. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Assertion xpab x | φ × y | ψ = x y | φ ψ

Proof

Step Hyp Ref Expression
1 relxp Rel x | φ × y | ψ
2 relopabv Rel x y | φ ψ
3 df-clab a x | φ a x φ
4 df-clab b y | ψ b y ψ
5 3 4 anbi12i a x | φ b y | ψ a x φ b y ψ
6 sban b y φ ψ b y φ b y ψ
7 sbsbc b y φ ψ [˙b / y]˙ φ ψ
8 sbv b y φ φ
9 8 anbi1i b y φ b y ψ φ b y ψ
10 6 7 9 3bitr3i [˙b / y]˙ φ ψ φ b y ψ
11 10 sbbii a x [˙b / y]˙ φ ψ a x φ b y ψ
12 sbsbc a x [˙b / y]˙ φ ψ [˙a / x]˙ [˙b / y]˙ φ ψ
13 sban a x φ b y ψ a x φ a x b y ψ
14 sbv a x b y ψ b y ψ
15 14 anbi2i a x φ a x b y ψ a x φ b y ψ
16 13 15 bitri a x φ b y ψ a x φ b y ψ
17 11 12 16 3bitr3i [˙a / x]˙ [˙b / y]˙ φ ψ a x φ b y ψ
18 5 17 bitr4i a x | φ b y | ψ [˙a / x]˙ [˙b / y]˙ φ ψ
19 brxp a x | φ × y | ψ b a x | φ b y | ψ
20 eqid x y | φ ψ = x y | φ ψ
21 20 brabsb a x y | φ ψ b [˙a / x]˙ [˙b / y]˙ φ ψ
22 18 19 21 3bitr4i a x | φ × y | ψ b a x y | φ ψ b
23 1 2 22 eqbrriv x | φ × y | ψ = x y | φ ψ