Metamath Proof Explorer

Theorem opelres

Description: Ordered pair elementhood in a restriction. Exercise 13 of TakeutiZaring p. 25. (Contributed by NM, 13-Nov-1995) (Revised by BJ, 18-Feb-2022) Commute the consequent. (Revised by Peter Mazsa, 24-Sep-2022)

		Ref	Expression
	Assertion	opelres	$⊢ C \in V \to (⟨B, C⟩ \in ({R ↾}_{A}) \leftrightarrow (B \in A \land ⟨B, C⟩ \in R))$

Proof

Step	Hyp	Ref	Expression
1		df-res	$⊢ {R ↾}_{A} = R \cap (A \times V)$
2	1	elin2	$⊢ ⟨B, C⟩ \in ({R ↾}_{A}) \leftrightarrow (⟨B, C⟩ \in R \land ⟨B, C⟩ \in (A \times V))$
3		opelxp	$⊢ ⟨B, C⟩ \in (A \times V) \leftrightarrow (B \in A \land C \in V)$
4		elex	$⊢ C \in V \to C \in V$
5	4	biantrud	$⊢ C \in V \to (B \in A \leftrightarrow (B \in A \land C \in V))$
6	3 5	bitr4id	$⊢ C \in V \to (⟨B, C⟩ \in (A \times V) \leftrightarrow B \in A)$
7	6	anbi1cd	$⊢ C \in V \to ((⟨B, C⟩ \in R \land ⟨B, C⟩ \in (A \times V)) \leftrightarrow (B \in A \land ⟨B, C⟩ \in R))$
8	2 7	syl5bb	$⊢ C \in V \to (⟨B, C⟩ \in ({R ↾}_{A}) \leftrightarrow (B \in A \land ⟨B, C⟩ \in R))$