# Metamath Proof Explorer

## Theorem funssres

Description: The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994)

Ref Expression
Assertion funssres ( ( Fun 𝐹𝐺𝐹 ) → ( 𝐹 ↾ dom 𝐺 ) = 𝐺 )

### Proof

Step Hyp Ref Expression
1 vex 𝑥 ∈ V
2 vex 𝑦 ∈ V
3 1 2 opeldm ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺𝑥 ∈ dom 𝐺 )
4 3 a1i ( 𝐺𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺𝑥 ∈ dom 𝐺 ) )
5 ssel ( 𝐺𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
6 4 5 jcad ( 𝐺𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
7 6 adantl ( ( Fun 𝐹𝐺𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
8 funeu2 ( ( Fun 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → ∃! 𝑦𝑥 , 𝑦 ⟩ ∈ 𝐹 )
9 1 eldm2 ( 𝑥 ∈ dom 𝐺 ↔ ∃ 𝑦𝑥 , 𝑦 ⟩ ∈ 𝐺 )
10 5 ancrd ( 𝐺𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
11 10 eximdv ( 𝐺𝐹 → ( ∃ 𝑦𝑥 , 𝑦 ⟩ ∈ 𝐺 → ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
12 9 11 syl5bi ( 𝐺𝐹 → ( 𝑥 ∈ dom 𝐺 → ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
13 12 imp ( ( 𝐺𝐹𝑥 ∈ dom 𝐺 ) → ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
14 eupick ( ( ∃! 𝑦𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
15 8 13 14 syl2an ( ( ( Fun 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ∧ ( 𝐺𝐹𝑥 ∈ dom 𝐺 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
16 15 exp43 ( Fun 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝐺𝐹 → ( 𝑥 ∈ dom 𝐺 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) ) ) )
17 16 com23 ( Fun 𝐹 → ( 𝐺𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) ) ) )
18 17 imp ( ( Fun 𝐹𝐺𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) ) )
19 18 com34 ( ( Fun 𝐹𝐺𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) ) )
20 19 pm2.43d ( ( Fun 𝐹𝐺𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ dom 𝐺 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
21 20 impcomd ( ( Fun 𝐹𝐺𝐹 ) → ( ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
22 7 21 impbid ( ( Fun 𝐹𝐺𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ↔ ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
23 2 opelresi ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ dom 𝐺 ) ↔ ( 𝑥 ∈ dom 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
24 22 23 syl6rbbr ( ( Fun 𝐹𝐺𝐹 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ dom 𝐺 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
25 24 alrimivv ( ( Fun 𝐹𝐺𝐹 ) → ∀ 𝑥𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ dom 𝐺 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
26 relres Rel ( 𝐹 ↾ dom 𝐺 )
27 funrel ( Fun 𝐹 → Rel 𝐹 )
28 relss ( 𝐺𝐹 → ( Rel 𝐹 → Rel 𝐺 ) )
29 27 28 mpan9 ( ( Fun 𝐹𝐺𝐹 ) → Rel 𝐺 )
30 eqrel ( ( Rel ( 𝐹 ↾ dom 𝐺 ) ∧ Rel 𝐺 ) → ( ( 𝐹 ↾ dom 𝐺 ) = 𝐺 ↔ ∀ 𝑥𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ dom 𝐺 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
31 26 29 30 sylancr ( ( Fun 𝐹𝐺𝐹 ) → ( ( 𝐹 ↾ dom 𝐺 ) = 𝐺 ↔ ∀ 𝑥𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ dom 𝐺 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ) )
32 25 31 mpbird ( ( Fun 𝐹𝐺𝐹 ) → ( 𝐹 ↾ dom 𝐺 ) = 𝐺 )