Theorem vxp

Description: Cartesian product of the universe and a class. (Contributed by Peter Mazsa, 3-Dec-2020)

	Ref	Expression
Assertion	vxp	⊢ ( V × 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 ∈ 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		xpv	⊢ ( 𝐴 × V ) = { ⟨ 𝑦 , 𝑥 ⟩ ∣ 𝑦 ∈ 𝐴 }
2	1	cnveqi	⊢ ◡ ( 𝐴 × V ) = ◡ { ⟨ 𝑦 , 𝑥 ⟩ ∣ 𝑦 ∈ 𝐴 }
3		cnvxp	⊢ ◡ ( 𝐴 × V ) = ( V × 𝐴 )
4		cnvopab	⊢ ◡ { ⟨ 𝑦 , 𝑥 ⟩ ∣ 𝑦 ∈ 𝐴 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 ∈ 𝐴 }
5	2 3 4	3eqtr3i	⊢ ( V × 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 ∈ 𝐴 }