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

Metamath Proof Explorer

Theorem relres

Description: A restriction is a relation. Exercise 12 of TakeutiZaring p. 25. (Contributed by NM, 2-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	relres	$⊢ Rel ({A ↾}_{B})$

Proof

Step	Hyp	Ref	Expression
1		df-res	$⊢ {A ↾}_{B} = A \cap (B \times V)$
2		inss2	$⊢ A \cap (B \times V) \subseteq B \times V$
3	1 2	eqsstri	$⊢ {A ↾}_{B} \subseteq B \times V$
4		relxp	$⊢ Rel (B \times V)$
5		relss	$⊢ {A ↾}_{B} \subseteq B \times V \to (Rel (B \times V) \to Rel ({A ↾}_{B}))$
6	3 4 5	mp2	$⊢ Rel ({A ↾}_{B})$