let UN be Universe; :: thesis: for X being set st id X is Element of UN holds
X is Element of UN
let X be set ; :: thesis: ( id X is Element of UN implies X is Element of UN )
assume id X is Element of UN ; :: thesis: X is Element of UN
then dom (id X) in UN by Th37;
hence X is Element of UN by RELAT_1:45; :: thesis: verum