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

Metamath Proof Explorer

Theorem elopabran

Description: Membership in an ordered-pair class abstraction defined by a restricted binary relation. (Contributed by AV, 16-Feb-2021)

		Ref	Expression
	Assertion	elopabran	$⊢ A \in \{⟨x, y⟩ \| (x R y \land ψ)\} \to A \in R$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (x R y \land ψ) \to x R y$
2	1	ssopab2i	$⊢ \{⟨x, y⟩ \| (x R y \land ψ)\} \subseteq \{⟨x, y⟩ \| x R y\}$
3		opabss	$⊢ \{⟨x, y⟩ \| x R y\} \subseteq R$
4	2 3	sstri	$⊢ \{⟨x, y⟩ \| (x R y \land ψ)\} \subseteq R$
5	4	sseli	$⊢ A \in \{⟨x, y⟩ \| (x R y \land ψ)\} \to A \in R$