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

Theorem fndmin 5567
 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 5507 . . . . . 6
2 df-mpt 4023 . . . . . 6
31, 2eqtrdi 2203 . . . . 5
4 dffn5im 5507 . . . . . 6
5 df-mpt 4023 . . . . . 6
64, 5eqtrdi 2203 . . . . 5
73, 6ineqan12d 3306 . . . 4
8 inopab 4711 . . . 4
97, 8eqtrdi 2203 . . 3
109dmeqd 4781 . 2
11 anandi 580 . . . . . . . 8
1211exbii 1582 . . . . . . 7
13 19.42v 1883 . . . . . . 7
1412, 13bitr3i 185 . . . . . 6
15 funfvex 5478 . . . . . . . . 9
16 eqeq1 2161 . . . . . . . . . 10
1716ceqsexgv 2838 . . . . . . . . 9
1815, 17syl 14 . . . . . . . 8
1918funfni 5263 . . . . . . 7
2019pm5.32da 448 . . . . . 6
2114, 20syl5bb 191 . . . . 5
2221abbidv 2272 . . . 4
23 dmopab 4790 . . . 4
24 df-rab 2441 . . . 4
2522, 23, 243eqtr4g 2212 . . 3