Help request: Fraenkel term definition

 Hello. I am having trouble finding Mizar's definition of the
 Fraenkel term, and more generally, what definitions are hidden.

 After reading the scheme axiom at TARSKI:sch 1 and looking around the
 rest of the MML, I don't understand how the constructor-like notation:
        { x : P[x] }
 is defined. It's as if there is an invisible Mizar declaration resembling:

        func { x : P[x] } means y in it iff ex x st y = x & P[x];

 Yet, I don't see it in hidden.miz.  How does one know what definitions
 are available but hidden?

 Thanks
 - Greg Frascadore