Metamath Proof Explorer

Theorem opabbrex

Description: A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by BJ/AV, 20-Jun-2019) (Proof shortened by OpenAI, 25-Mar-2020)

		Ref	Expression
	Assertion	opabbrex	$⊢ (\forall x \forall y (x R y \to φ) \land \{⟨x, y⟩ \| φ\} \in V) \to \{⟨x, y⟩ \| (x R y \land ψ)\} \in V$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (\forall x \forall y (x R y \to φ) \land \{⟨x, y⟩ \| φ\} \in V) \to \{⟨x, y⟩ \| φ\} \in V$
2		pm3.41	$⊢ (x R y \to φ) \to ((x R y \land ψ) \to φ)$
3	2	2alimi	$⊢ \forall x \forall y (x R y \to φ) \to \forall x \forall y ((x R y \land ψ) \to φ)$
4	3	adantr	$⊢ (\forall x \forall y (x R y \to φ) \land \{⟨x, y⟩ \| φ\} \in V) \to \forall x \forall y ((x R y \land ψ) \to φ)$
5		ssopab2	$⊢ \forall x \forall y ((x R y \land ψ) \to φ) \to \{⟨x, y⟩ \| (x R y \land ψ)\} \subseteq \{⟨x, y⟩ \| φ\}$
6	4 5	syl	$⊢ (\forall x \forall y (x R y \to φ) \land \{⟨x, y⟩ \| φ\} \in V) \to \{⟨x, y⟩ \| (x R y \land ψ)\} \subseteq \{⟨x, y⟩ \| φ\}$
7	1 6	ssexd	$⊢ (\forall x \forall y (x R y \to φ) \land \{⟨x, y⟩ \| φ\} \in V) \to \{⟨x, y⟩ \| (x R y \land ψ)\} \in V$