relssres

Description: Simplification law for restriction. (Contributed by NM, 16-Aug-1994)

		Ref	Expression
	Assertion	relssres	$⊢ (Rel A \land dom A \subseteq B) \to {A ↾}_{B} = A$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (Rel A \land dom A \subseteq B) \to Rel A$
2		vex	$⊢ x \in V$
3		vex	$⊢ y \in V$
4	2 3	opeldm	$⊢ ⟨x, y⟩ \in A \to x \in dom A$
5		ssel	$⊢ dom A \subseteq B \to (x \in dom A \to x \in B)$
6	4 5	syl5	$⊢ dom A \subseteq B \to (⟨x, y⟩ \in A \to x \in B)$
7	6	ancrd	$⊢ dom A \subseteq B \to (⟨x, y⟩ \in A \to (x \in B \land ⟨x, y⟩ \in A))$
8	3	opelresi	$⊢ ⟨x, y⟩ \in ({A ↾}_{B}) \leftrightarrow (x \in B \land ⟨x, y⟩ \in A)$
9	7 8	imbitrrdi	$⊢ dom A \subseteq B \to (⟨x, y⟩ \in A \to ⟨x, y⟩ \in ({A ↾}_{B}))$
10	9	adantl	$⊢ (Rel A \land dom A \subseteq B) \to (⟨x, y⟩ \in A \to ⟨x, y⟩ \in ({A ↾}_{B}))$
11	1 10	relssdv	$⊢ (Rel A \land dom A \subseteq B) \to A \subseteq {A ↾}_{B}$
12		resss	$⊢ {A ↾}_{B} \subseteq A$
13	11 12	jctil	$⊢ (Rel A \land dom A \subseteq B) \to ({A ↾}_{B} \subseteq A \land A \subseteq {A ↾}_{B})$
14		eqss	$⊢ {A ↾}_{B} = A \leftrightarrow ({A ↾}_{B} \subseteq A \land A \subseteq {A ↾}_{B})$
15	13 14	sylibr	$⊢ (Rel A \land dom A \subseteq B) \to {A ↾}_{B} = A$

Metamath Proof Explorer