Metamath Proof Explorer

Theorem opabresex0d

Description: A collection of ordered pairs, the class of all possible second components being a set, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 1-Jan-2021)

		Ref	Expression
	Hypotheses	opabresex0d.x	$⊢ (φ \land x R y) \to x \in C$
		opabresex0d.t	$⊢ (φ \land x R y) \to θ$
		opabresex0d.y	$⊢ (φ \land x \in C) \to \{y \| θ\} \in V$
		opabresex0d.c	$⊢ φ \to C \in W$
	Assertion	opabresex0d	$⊢ φ \to \{⟨x, y⟩ \| (x R y \land ψ)\} \in V$

Proof

Step	Hyp	Ref	Expression
1		opabresex0d.x	$⊢ (φ \land x R y) \to x \in C$
2		opabresex0d.t	$⊢ (φ \land x R y) \to θ$
3		opabresex0d.y	$⊢ (φ \land x \in C) \to \{y \| θ\} \in V$
4		opabresex0d.c	$⊢ φ \to C \in W$
5	1 2	jca	$⊢ (φ \land x R y) \to (x \in C \land θ)$
6	5	ex	$⊢ φ \to (x R y \to (x \in C \land θ))$
7	6	alrimivv	$⊢ φ \to \forall x \forall y (x R y \to (x \in C \land θ))$
8	3	elexd	$⊢ (φ \land x \in C) \to \{y \| θ\} \in V$
9	4 8	opabex3d	$⊢ φ \to \{⟨x, y⟩ \| (x \in C \land θ)\} \in V$
10		opabbrex	$⊢ (\forall x \forall y (x R y \to (x \in C \land θ)) \land \{⟨x, y⟩ \| (x \in C \land θ)\} \in V) \to \{⟨x, y⟩ \| (x R y \land ψ)\} \in V$
11	7 9 10	syl2anc	$⊢ φ \to \{⟨x, y⟩ \| (x R y \land ψ)\} \in V$