Theorem xpv

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

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

Proof

Step	Hyp	Ref	Expression
1		df-xp	|- ( A X. _V ) = { <. x , y >. | ( x e. A /\ y e. _V ) }
2		vex	|- y e. _V
3		iba	|- ( y e. _V -> ( x e. A <-> ( x e. A /\ y e. _V ) ) )
4	2 3	ax-mp	|- ( x e. A <-> ( x e. A /\ y e. _V ) )
5	4	opabbii	|- { <. x , y >. | x e. A } = { <. x , y >. | ( x e. A /\ y e. _V ) }
6	1 5	eqtr4i	|- ( A X. _V ) = { <. x , y >. | x e. A }