Theorem xpv

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

	Ref	Expression
Assertion	xpv	⊢ ( 𝐴 × V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		df-xp	⊢ ( 𝐴 × V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ V ) }
2		vex	⊢ 𝑦 ∈ V
3		iba	⊢ ( 𝑦 ∈ V → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ V ) ) )
4	2 3	ax-mp	⊢ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ V ) )
5	4	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝐴 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ V ) }
6	1 5	eqtr4i	⊢ ( 𝐴 × V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝐴 }