Theorem xpab

Description: Cartesian 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	⊢ ( { 𝑥 ∣ 𝜑 } × { 𝑦 ∣ 𝜓 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) }