Theorem xpv

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

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

Proof

Step	Hyp	Ref	Expression
1		df-xp	$$⊢A\times \mathrm{V}=\left\{⟨x,y⟩|\left(x\in A\wedge y\in \mathrm{V}\right)\right\}$$
2		vex	$$⊢y\in \mathrm{V}$$
3		iba	$$⊢y\in \mathrm{V}\to \left(x\in A\leftrightarrow \left(x\in A\wedge y\in \mathrm{V}\right)\right)$$
4	2 3	ax-mp	$$⊢x\in A\leftrightarrow \left(x\in A\wedge y\in \mathrm{V}\right)$$
5	4	opabbii	$$⊢\left\{⟨x,y⟩|x\in A\right\}=\left\{⟨x,y⟩|\left(x\in A\wedge y\in \mathrm{V}\right)\right\}$$
6	1 5	eqtr4i	$$⊢A\times \mathrm{V}=\left\{⟨x,y⟩|x\in A\right\}$$