Theorem xp2

Description: Representation of Cartesian product based on ordered pair component functions. (Contributed by NM, 16-Sep-2006)

	Ref	Expression
Assertion	xp2	⊢ ( 𝐴 × 𝐵 ) = { 𝑥 ∈ ( V × V ) ∣ ( ( 1st ‘ 𝑥 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝑥 ) ∈ 𝐵 ) }

Proof

Step	Hyp	Ref	Expression
1		elxp7	⊢ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝑥 ) ∈ 𝐵 ) ) )
2	1	eqabi	⊢ ( 𝐴 × 𝐵 ) = { 𝑥 ∣ ( 𝑥 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝑥 ) ∈ 𝐵 ) ) }
3		df-rab	⊢ { 𝑥 ∈ ( V × V ) ∣ ( ( 1st ‘ 𝑥 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝑥 ) ∈ 𝐵 ) } = { 𝑥 ∣ ( 𝑥 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝑥 ) ∈ 𝐵 ) ) }
4	2 3	eqtr4i	⊢ ( 𝐴 × 𝐵 ) = { 𝑥 ∈ ( V × V ) ∣ ( ( 1st ‘ 𝑥 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝑥 ) ∈ 𝐵 ) }