[mizar] Scheme for func definition with Fraenkel operator?

[Freek Wiedijk <freek@cs.kun.nl>]

Hi everone,

First of all, a very happy new year!

Then my question :-)  Suppose I define a functor like this:

  definition
   func foo args equals :Def: { x : P[x,args] };
   ...
  end;

Then it would be nice to have as a theorem:

  theorem Th: x in foo args iff P[x,args];

But I just got the impression that putting "by Def" as a proof
doesn't work!  So it's easy to put a more involved proof using Def.
But I wonder now:

 (a) what _is_ the statement "Def"? (clearly it's not "Th")

and

 (b) wouldn't it be nice to have a scheme "Sch" so that I would
     be able to prove "Th" by just putting "... from Sch(Def);"

So: does such a scheme already exist?  And if so, which one is it?

Freek