Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  fndmin Unicode version

Theorem fndmin 5306
 Description: Two ways to express the locus of equality between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
Assertion
Ref Expression
fndmin
Distinct variable groups:   ,   ,   ,

Proof of Theorem fndmin
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dffn5im 5251 . . . . . 6
2 df-mpt 3849 . . . . . 6
31, 2syl6eq 2130 . . . . 5
4 dffn5im 5251 . . . . . 6
5 df-mpt 3849 . . . . . 6
64, 5syl6eq 2130 . . . . 5
73, 6ineqan12d 3176 . . . 4
8 inopab 4496 . . . 4
97, 8syl6eq 2130 . . 3
109dmeqd 4565 . 2
11 anandi 555 . . . . . . . 8
1211exbii 1537 . . . . . . 7
13 19.42v 1828 . . . . . . 7
1412, 13bitr3i 184 . . . . . 6
15 funfvex 5223 . . . . . . . . 9
16 eqeq1 2088 . . . . . . . . . 10
1716ceqsexgv 2725 . . . . . . . . 9
1815, 17syl 14 . . . . . . . 8
1918funfni 5030 . . . . . . 7
2019pm5.32da 440 . . . . . 6
2114, 20syl5bb 190 . . . . 5
2221abbidv 2197 . . . 4
23 dmopab 4574 . . . 4
24 df-rab 2358 . . . 4
2522, 23, 243eqtr4g 2139 . . 3