let a, c, x, w, b, d, y, z be set ; ( a,c,x,w are_mutually_different implies a,c,x,w --> b,d,y,z = {[a,b],[c,d],[x,y],[w,z]} )
assume A1:
a,c,x,w are_mutually_different
; a,c,x,w --> b,d,y,z = {[a,b],[c,d],[x,y],[w,z]}
then A2:
a <> c
by ZFMISC_1:def 6;
A3:
a <> x
by A1, ZFMISC_1:def 6;
A4:
a <> w
by A1, ZFMISC_1:def 6;
A5:
c <> x
by A1, ZFMISC_1:def 6;
A6:
c <> w
by A1, ZFMISC_1:def 6;
A7:
x <> w
by A1, ZFMISC_1:def 6;
set m = a,c --> b,d;
set n = x,w --> y,z;
A8:
dom (a,c --> b,d) = {a,c}
by FUNCT_4:65;
A9:
dom (x,w --> y,z) = {x,w}
by FUNCT_4:65;
A10:
not a in {x,w}
by A3, A4, TARSKI:def 2;
not c in {x,w}
by A5, A6, TARSKI:def 2;
then a,c,x,w --> b,d,y,z =
(a,c --> b,d) \/ (x,w --> y,z)
by A8, A9, A10, FUNCT_4:32, ZFMISC_1:57
.=
{[a,b],[c,d]} \/ (x,w --> y,z)
by A2, FUNCT_4:71
.=
{[a,b],[c,d]} \/ {[x,y],[w,z]}
by A7, FUNCT_4:71
.=
{[a,b],[c,d],[x,y],[w,z]}
by ENUMSET1:45
;
hence
a,c,x,w --> b,d,y,z = {[a,b],[c,d],[x,y],[w,z]}
; verum