resieq

Description: A restricted identity relation is equivalent to equality in its domain. (Contributed by NM, 30-Apr-2004)

		Ref	Expression
	Assertion	resieq	$⊢ (B \in A \land C \in A) \to (B ({I ↾}_{A}) C \leftrightarrow B = C)$

Step	Hyp	Ref	Expression
1		breq2	$⊢ x = C \to (B ({I ↾}_{A}) x \leftrightarrow B ({I ↾}_{A}) C)$
2		eqeq2	$⊢ x = C \to (B = x \leftrightarrow B = C)$
3	1 2	bibi12d	$⊢ x = C \to ((B ({I ↾}_{A}) x \leftrightarrow B = x) \leftrightarrow (B ({I ↾}_{A}) C \leftrightarrow B = C))$
4	3	imbi2d	$⊢ x = C \to ((B \in A \to (B ({I ↾}_{A}) x \leftrightarrow B = x)) \leftrightarrow (B \in A \to (B ({I ↾}_{A}) C \leftrightarrow B = C)))$
5		vex	$⊢ x \in V$
6	5	opres	$⊢ B \in A \to (⟨B, x⟩ \in ({I ↾}_{A}) \leftrightarrow ⟨B, x⟩ \in I)$
7		df-br	$⊢ B ({I ↾}_{A}) x \leftrightarrow ⟨B, x⟩ \in ({I ↾}_{A})$
8	5	ideq	$⊢ B I x \leftrightarrow B = x$
9		df-br	$⊢ B I x \leftrightarrow ⟨B, x⟩ \in I$
10	8 9	bitr3i	$⊢ B = x \leftrightarrow ⟨B, x⟩ \in I$
11	6 7 10	3bitr4g	$⊢ B \in A \to (B ({I ↾}_{A}) x \leftrightarrow B = x)$
12	4 11	vtoclg	$⊢ C \in A \to (B \in A \to (B ({I ↾}_{A}) C \leftrightarrow B = C))$
13	12	impcom	$⊢ (B \in A \land C \in A) \to (B ({I ↾}_{A}) C \leftrightarrow B = C)$

Metamath Proof Explorer