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

Metamath Proof Explorer

Theorem opabss

Description: The collection of ordered pairs in a class is a subclass of it. (Contributed by NM, 27-Dec-1996) (Proof shortened by Andrew Salmon, 9-Jul-2011)

		Ref	Expression
	Assertion	opabss	$⊢ \{⟨x, y⟩ \| x R y\} \subseteq R$

Proof

Step	Hyp	Ref	Expression
1		df-opab	$⊢ \{⟨x, y⟩ \| x R y\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land x R y)\}$
2		df-br	$⊢ x R y \leftrightarrow ⟨x, y⟩ \in R$
3		eleq1	$⊢ z = ⟨x, y⟩ \to (z \in R \leftrightarrow ⟨x, y⟩ \in R)$
4	3	biimpar	$⊢ (z = ⟨x, y⟩ \land ⟨x, y⟩ \in R) \to z \in R$
5	2 4	sylan2b	$⊢ (z = ⟨x, y⟩ \land x R y) \to z \in R$
6	5	exlimivv	$⊢ \exists x \exists y (z = ⟨x, y⟩ \land x R y) \to z \in R$
7	6	abssi	$⊢ \{z \| \exists x \exists y (z = ⟨x, y⟩ \land x R y)\} \subseteq R$
8	1 7	eqsstri	$⊢ \{⟨x, y⟩ \| x R y\} \subseteq R$