Theorem vxp

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

	Ref	Expression
Assertion	vxp	$$⊢\mathrm{V}\times A=\left\{⟨x,y⟩|y\in A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		xpv	$$⊢A\times \mathrm{V}=\left\{⟨y,x⟩|y\in A\right\}$$
2	1	cnveqi	$$⊢{\left(A\times \mathrm{V}\right)}^{-1}={\left\{⟨y,x⟩|y\in A\right\}}^{-1}$$
3		cnvxp	$$⊢{\left(A\times \mathrm{V}\right)}^{-1}=\mathrm{V}\times A$$
4		cnvopab	$$⊢{\left\{⟨y,x⟩|y\in A\right\}}^{-1}=\left\{⟨x,y⟩|y\in A\right\}$$
5	2 3 4	3eqtr3i	$$⊢\mathrm{V}\times A=\left\{⟨x,y⟩|y\in A\right\}$$