Metamath Proof Explorer

Theorem relssres

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

Ref Expression
Assertion relssres ⊢ Rel ⁡ A ∧ dom ⁡ A ⊆ B → A ↾ B = A

Proof

Step Hyp Ref Expression
1 simpl ⊢ Rel ⁡ A ∧ dom ⁡ A ⊆ B → Rel ⁡ A
2 vex ⊢ x ∈ V
3 vex ⊢ y ∈ V
4 2 3 opeldm ⊢ x y ∈ A → x ∈ dom ⁡ A
5 ssel ⊢ dom ⁡ A ⊆ B → x ∈ dom ⁡ A → x ∈ B
6 4 5 syl5 ⊢ dom ⁡ A ⊆ B → x y ∈ A → x ∈ B
7 6 ancrd ⊢ dom ⁡ A ⊆ B → x y ∈ A → x ∈ B ∧ x y ∈ A
8 3 opelresi ⊢ x y ∈ A ↾ B ↔ x ∈ B ∧ x y ∈ A
9 7 8 syl6ibr ⊢ dom ⁡ A ⊆ B → x y ∈ A → x y ∈ A ↾ B
10 9 adantl ⊢ Rel ⁡ A ∧ dom ⁡ A ⊆ B → x y ∈ A → x y ∈ A ↾ B
11 1 10 relssdv ⊢ Rel ⁡ A ∧ dom ⁡ A ⊆ B → A ⊆ A ↾ B
12 resss ⊢ A ↾ B ⊆ A
13 11 12 jctil ⊢ Rel ⁡ A ∧ dom ⁡ A ⊆ B → A ↾ B ⊆ A ∧ A ⊆ A ↾ B
14 eqss ⊢ A ↾ B = A ↔ A ↾ B ⊆ A ∧ A ⊆ A ↾ B
15 13 14 sylibr ⊢ Rel ⁡ A ∧ dom ⁡ A ⊆ B → A ↾ B = A