Theorem bj-opabssvv

Description: A variant of relopabiv (which could be proved from it, similarly to relxp from xpss ). (Contributed by BJ, 28-Dec-2023)

	Ref	Expression
Assertion	bj-opabssvv	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ ( V × V )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	pm3.2i	⊢ ( 𝑥 ∈ V ∧ 𝑦 ∈ V )
4	3	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) )
5	4	ssopab2i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) }
6		df-xp	⊢ ( V × V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) }
7	5 6	sseqtrri	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ ( V × V )