Metamath Proof Explorer

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	$⊢ \{⟨x, y⟩ \| φ\} \subseteq V \times V$

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		vex	$⊢ y \in V$
3	1 2	pm3.2i	$⊢ (x \in V \land y \in V)$
4	3	a1i	$⊢ φ \to (x \in V \land y \in V)$
5	4	ssopab2i	$⊢ \{⟨x, y⟩ \| φ\} \subseteq \{⟨x, y⟩ \| (x \in V \land y \in V)\}$
6		df-xp	$⊢ V \times V = \{⟨x, y⟩ \| (x \in V \land y \in V)\}$
7	5 6	sseqtrri	$⊢ \{⟨x, y⟩ \| φ\} \subseteq V \times V$