This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opabresex2

Description: Restrictions of a collection of ordered pairs of related elements are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 15-Jan-2021) Add disjoint variable conditions betweem W , G and x , y to remove hypotheses. (Revised by SN, 13-Dec-2024)

		Ref	Expression
	Assertion	opabresex2	$⊢ \{⟨x, y⟩ \| (x W (G) y \land θ)\} \in V$

Proof

Step	Hyp	Ref	Expression
1		fvex	$⊢ W (G) \in V$
2		elopabran	$⊢ z \in \{⟨x, y⟩ \| (x W (G) y \land θ)\} \to z \in W (G)$
3	2	ssriv	$⊢ \{⟨x, y⟩ \| (x W (G) y \land θ)\} \subseteq W (G)$
4	1 3	ssexi	$⊢ \{⟨x, y⟩ \| (x W (G) y \land θ)\} \in V$