Metamath Proof Explorer

Theorem opelresi

Description: Ordered pair membership in a restriction. Exercise 13 of TakeutiZaring p. 25. (Contributed by NM, 13-Nov-1995)

		Ref	Expression
	Hypothesis	opelresi.1	$⊢ C \in V$
	Assertion	opelresi	$⊢ ⟨B, C⟩ \in ({R ↾}_{A}) \leftrightarrow (B \in A \land ⟨B, C⟩ \in R)$

Step	Hyp	Ref	Expression
1		opelresi.1	$⊢ C \in V$
2		opelres	$⊢ C \in V \to (⟨B, C⟩ \in ({R ↾}_{A}) \leftrightarrow (B \in A \land ⟨B, C⟩ \in R))$
3	1 2	ax-mp	$⊢ ⟨B, C⟩ \in ({R ↾}_{A}) \leftrightarrow (B \in A \land ⟨B, C⟩ \in R)$