Metamath Proof Explorer


Theorem xpab

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

Ref Expression
Assertion xpab ( { 𝑥𝜑 } × { 𝑦𝜓 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑𝜓 ) }

Proof

Step Hyp Ref Expression
1 relxp Rel ( { 𝑥𝜑 } × { 𝑦𝜓 } )
2 relopabv Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑𝜓 ) }
3 df-clab ( 𝑎 ∈ { 𝑥𝜑 } ↔ [ 𝑎 / 𝑥 ] 𝜑 )
4 df-clab ( 𝑏 ∈ { 𝑦𝜓 } ↔ [ 𝑏 / 𝑦 ] 𝜓 )
5 3 4 anbi12i ( ( 𝑎 ∈ { 𝑥𝜑 } ∧ 𝑏 ∈ { 𝑦𝜓 } ) ↔ ( [ 𝑎 / 𝑥 ] 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) )
6 sban ( [ 𝑏 / 𝑦 ] ( 𝜑𝜓 ) ↔ ( [ 𝑏 / 𝑦 ] 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) )
7 sbsbc ( [ 𝑏 / 𝑦 ] ( 𝜑𝜓 ) ↔ [ 𝑏 / 𝑦 ] ( 𝜑𝜓 ) )
8 sbv ( [ 𝑏 / 𝑦 ] 𝜑𝜑 )
9 8 anbi1i ( ( [ 𝑏 / 𝑦 ] 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) ↔ ( 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) )
10 6 7 9 3bitr3i ( [ 𝑏 / 𝑦 ] ( 𝜑𝜓 ) ↔ ( 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) )
11 10 sbbii ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] ( 𝜑𝜓 ) ↔ [ 𝑎 / 𝑥 ] ( 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) )
12 sbsbc ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] ( 𝜑𝜓 ) ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] ( 𝜑𝜓 ) )
13 sban ( [ 𝑎 / 𝑥 ] ( 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) ↔ ( [ 𝑎 / 𝑥 ] 𝜑 ∧ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ) )
14 sbv ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ↔ [ 𝑏 / 𝑦 ] 𝜓 )
15 14 anbi2i ( ( [ 𝑎 / 𝑥 ] 𝜑 ∧ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ) ↔ ( [ 𝑎 / 𝑥 ] 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) )
16 13 15 bitri ( [ 𝑎 / 𝑥 ] ( 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) ↔ ( [ 𝑎 / 𝑥 ] 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) )
17 11 12 16 3bitr3i ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] ( 𝜑𝜓 ) ↔ ( [ 𝑎 / 𝑥 ] 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) )
18 5 17 bitr4i ( ( 𝑎 ∈ { 𝑥𝜑 } ∧ 𝑏 ∈ { 𝑦𝜓 } ) ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] ( 𝜑𝜓 ) )
19 brxp ( 𝑎 ( { 𝑥𝜑 } × { 𝑦𝜓 } ) 𝑏 ↔ ( 𝑎 ∈ { 𝑥𝜑 } ∧ 𝑏 ∈ { 𝑦𝜓 } ) )
20 eqid { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑𝜓 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑𝜓 ) }
21 20 brabsb ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑𝜓 ) } 𝑏[ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] ( 𝜑𝜓 ) )
22 18 19 21 3bitr4i ( 𝑎 ( { 𝑥𝜑 } × { 𝑦𝜓 } ) 𝑏𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑𝜓 ) } 𝑏 )
23 1 2 22 eqbrriv ( { 𝑥𝜑 } × { 𝑦𝜓 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑𝜓 ) }