let X, Y be set ; :: thesis: for U being Universe st X in U & Y in U holds
( [:X,Y:] in U & Funcs (X,Y) in U )
let U be Universe; :: thesis: ( X in U & Y in U implies ( [:X,Y:] in U & Funcs (X,Y) in U ) )
assume that
A1: X in U and
A2: Y in U ; :: thesis: ( [:X,Y:] in U & Funcs (X,Y) in U )
X \/ Y in U by A1, A2, Th60;
then bool (X \/ Y) in U by Th59;
then A3: bool (bool (X \/ Y)) in U by Th59;
[:X,Y:] c= bool (bool (X \/ Y)) by ZFMISC_1:86;
hence [:X,Y:] in U by A3, CLASSES1:def 1; :: thesis: Funcs (X,Y) in U
then A4: bool [:X,Y:] in U by Th59;
Funcs (X,Y) c= bool [:X,Y:] by FRAENKEL:2;
hence Funcs (X,Y) in U by A4, CLASSES1:def 1; :: thesis: verum