Metamath Proof Explorer


Theorem fnres

Description: An equivalence for functionality of a restriction. Compare dffun8 . (Contributed by Mario Carneiro, 20-May-2015) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion fnres F A Fn A x A ∃! y x F y

Proof

Step Hyp Ref Expression
1 ancom x A * y x F y x A y x F y x A y x F y x A * y x F y
2 vex y V
3 2 brresi x F A y x A x F y
4 3 mobii * y x F A y * y x A x F y
5 moanimv * y x A x F y x A * y x F y
6 4 5 bitri * y x F A y x A * y x F y
7 6 albii x * y x F A y x x A * y x F y
8 relres Rel F A
9 dffun6 Fun F A Rel F A x * y x F A y
10 8 9 mpbiran Fun F A x * y x F A y
11 df-ral x A * y x F y x x A * y x F y
12 7 10 11 3bitr4i Fun F A x A * y x F y
13 dmres dom F A = A dom F
14 inss1 A dom F A
15 13 14 eqsstri dom F A A
16 eqss dom F A = A dom F A A A dom F A
17 15 16 mpbiran dom F A = A A dom F A
18 dfss3 A dom F A x A x dom F A
19 13 elin2 x dom F A x A x dom F
20 19 baib x A x dom F A x dom F
21 vex x V
22 21 eldm x dom F y x F y
23 20 22 bitrdi x A x dom F A y x F y
24 23 ralbiia x A x dom F A x A y x F y
25 18 24 bitri A dom F A x A y x F y
26 17 25 bitri dom F A = A x A y x F y
27 12 26 anbi12i Fun F A dom F A = A x A * y x F y x A y x F y
28 r19.26 x A y x F y * y x F y x A y x F y x A * y x F y
29 1 27 28 3bitr4i Fun F A dom F A = A x A y x F y * y x F y
30 df-fn F A Fn A Fun F A dom F A = A
31 df-eu ∃! y x F y y x F y * y x F y
32 31 ralbii x A ∃! y x F y x A y x F y * y x F y
33 29 30 32 3bitr4i F A Fn A x A ∃! y x F y