bj-dfres2

Description: Alternate definition of the restriction of a class to another, as an ordered pair class abstraction: the restriction of a class to another is the class of ordered pairs whose first component is in the restricting class and whose components are related by the restricted class. (Contributed by Mario Carneiro, 5-Nov-2013) Do not depend on df-rel . (Revised by BJ, 16-Oct-2026) This is an alternate proof of dfres2 ; it is slightly shorter but not necessarily a gain (it uses bj-elres / elres , which uses bj-elinxp / elinxp ): dfres2 uses that both classes are relations ( relres and relopab ) to be able to use ordered-pair extensionality eqrelriiv : the latter's proof is long (considering the proofs of its parents up to ssrel ), but its usefulness makes it worth it.

		Ref	Expression
	Assertion	bj-dfres2	$⊢ {R ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land x R y)\}$

Proof

Step	Hyp	Ref	Expression
1		df-rex	$⊢ \exists x \in A \exists y (z = ⟨x, y⟩ \land x R y) \leftrightarrow \exists x (x \in A \land \exists y (z = ⟨x, y⟩ \land x R y))$
2		an12	$⊢ (z = ⟨x, y⟩ \land (x \in A \land x R y)) \leftrightarrow (x \in A \land (z = ⟨x, y⟩ \land x R y))$
3	2	exbii	$⊢ \exists y (z = ⟨x, y⟩ \land (x \in A \land x R y)) \leftrightarrow \exists y (x \in A \land (z = ⟨x, y⟩ \land x R y))$
4		19.42v	$⊢ \exists y (x \in A \land (z = ⟨x, y⟩ \land x R y)) \leftrightarrow (x \in A \land \exists y (z = ⟨x, y⟩ \land x R y))$
5	3 4	bitr2i	$⊢ (x \in A \land \exists y (z = ⟨x, y⟩ \land x R y)) \leftrightarrow \exists y (z = ⟨x, y⟩ \land (x \in A \land x R y))$
6	5	exbii	$⊢ \exists x (x \in A \land \exists y (z = ⟨x, y⟩ \land x R y)) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land x R y))$
7	1 6	bitri	$⊢ \exists x \in A \exists y (z = ⟨x, y⟩ \land x R y) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land x R y))$
8		bj-elres	$⊢ z \in ({R ↾}_{A}) \leftrightarrow \exists x \in A \exists y (z = ⟨x, y⟩ \land x R y)$
9		elopab	$⊢ z \in \{⟨x, y⟩ \| (x \in A \land x R y)\} \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land x R y))$
10	7 8 9	3bitr4i	$⊢ z \in ({R ↾}_{A}) \leftrightarrow z \in \{⟨x, y⟩ \| (x \in A \land x R y)\}$
11	10	eqriv	$⊢ {R ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land x R y)\}$

Metamath Proof Explorer

Theorem bj-dfres2

Proof