This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vxp

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

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

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