Theorem vxp

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

	Ref	Expression
Assertion	vxp	|- ( _V X. A ) = { <. x , y >. | y e. A }

Proof

Step	Hyp	Ref	Expression
1		xpv	|- ( A X. _V ) = { <. y , x >. | y e. A }
2	1	cnveqi	|- `' ( A X. _V ) = `' { <. y , x >. | y e. A }
3		cnvxp	|- `' ( A X. _V ) = ( _V X. A )
4		cnvopab	|- `' { <. y , x >. | y e. A } = { <. x , y >. | y e. A }
5	2 3 4	3eqtr3i	|- ( _V X. A ) = { <. x , y >. | y e. A }