let M be non empty set ; :: thesis: id M is_definable_in M
take H = (x. 3) '=' (x. 4); :: according to ZFMODEL1:def 3 :: thesis: ( Free H c= {(x. 3),(x. 4)} & M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) & id M = def_func H,M )
thus A1: Free H c= {(x. 3),(x. 4)} by ZF_LANG1:63; :: thesis: ( M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) & id M = def_func H,M )
reconsider i = id M as Function of M,M ;

now

let v be Function of VAR ,M; :: thesis: M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))))

now

let m3 be Element of M; :: thesis: M,v / (x. 3),m3 |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))

now

let m4 be Element of M; :: thesis: M,((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4 |= H <=> ((x. 4) '=' (x. 0 ))
A2: m3 = (v / (x. 3),m3) . (x. 3) by FUNCT_7:130;
A3: (((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4) . (x. 0 ) = ((v / (x. 3),m3) / (x. 0 ),m3) . (x. 0 ) by FUNCT_7:34, ZF_LANG1:86;
A4: ((v / (x. 3),m3) / (x. 0 ),m3) . (x. 0 ) = m3 by FUNCT_7:130;
A5: ((v / (x. 3),m3) / (x. 0 ),m3) . (x. 3) = (v / (x. 3),m3) . (x. 3) by FUNCT_7:34, ZF_LANG1:86;
A6: (((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4) . (x. 3) = ((v / (x. 3),m3) / (x. 0 ),m3) . (x. 3) by FUNCT_7:34, ZF_LANG1:86;

A7: now

assume M,((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4 |= H ; :: thesis: M,((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4 |= (x. 4) '=' (x. 0 )
then (((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4) . (x. 3) = (((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4) . (x. 4) by ZF_MODEL:12;
hence M,((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4 |= (x. 4) '=' (x. 0 ) by A6, A2, A5, A3, A4, ZF_MODEL:12; :: thesis: verum

end;

A8: (((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4) . (x. 4) = m4 by FUNCT_7:130;

now

assume M,((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4 |= (x. 4) '=' (x. 0 ) ; :: thesis: M,((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4 |= H
then m4 = m3 by A3, A4, A8, ZF_MODEL:12;
hence M,((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4 |= H by A6, A2, A5, A8, ZF_MODEL:12; :: thesis: verum

end;

hence M,((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4 |= H <=> ((x. 4) '=' (x. 0 )) by A7, ZF_MODEL:19; :: thesis: verum

end;

then M,(v / (x. 3),m3) / (x. 0 ),m3 |= All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))) by ZF_LANG1:80;
hence M,v / (x. 3),m3 |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))) by ZF_LANG1:82; :: thesis: verum

end;

hence M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) by ZF_LANG1:80; :: thesis: verum

end;

hence A9: M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) by ZF_MODEL:def 5; :: thesis: id M = def_func H,M

now

consider v being Function of VAR ,M;
let a be Element of M; :: thesis: i . a = (def_func H,M) . a
A10: a = (v / (x. 3),a) . (x. 3) by FUNCT_7:130;
A11: ((v / (x. 3),a) / (x. 4),a) . (x. 4) = a by FUNCT_7:130;
A12: ((v / (x. 3),a) / (x. 4),a) . (x. 3) = (v / (x. 3),a) . (x. 3) by FUNCT_7:34, ZF_LANG1:86;
then M,(v / (x. 3),a) / (x. 4),a |= H by A10, A11, ZF_MODEL:12;
then (def_func H,M) . a = a by A1, A9, A12, A10, A11, ZFMODEL1:def 2;
hence i . a = (def_func H,M) . a by FUNCT_1:35; :: thesis: verum

end;

hence id M = def_func H,M by FUNCT_2:113; :: thesis: verum