:: deftheorem defines is_definable_in ZFMODEL1:def 3 :
for F being Function
for E being non empty set holds
( F is_definable_in E iff ex H being ZF-formula st
( Free H c= {(x. 3),(x. 4)} & E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func (H,E) ) );