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 


-- 
View this message in context: http://www.nabble.com/Help-request%3A-Fraenkel-term-definition-tp20980174p20980174.html
Sent from the Mizar mailing list archive at Nabble.com.