Metamath Proof Explorer

Theorem xpab

Description: Cartesian 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 | φ ∧ ψ