let A be QC-alphabet ; for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A
for s, t being bound_QC-variable of A st Ex (x,y,z,p) = Ex (t,s,q) holds
( x = t & y = s & Ex (z,p) = q )
let x, y, z be bound_QC-variable of A; for p, q being Element of QC-WFF A
for s, t being bound_QC-variable of A st Ex (x,y,z,p) = Ex (t,s,q) holds
( x = t & y = s & Ex (z,p) = q )
let p, q be Element of QC-WFF A; for s, t being bound_QC-variable of A st Ex (x,y,z,p) = Ex (t,s,q) holds
( x = t & y = s & Ex (z,p) = q )
let s, t be bound_QC-variable of A; ( Ex (x,y,z,p) = Ex (t,s,q) implies ( x = t & y = s & Ex (z,p) = q ) )
assume A1:
Ex (x,y,z,p) = Ex (t,s,q)
; ( x = t & y = s & Ex (z,p) = q )
hence
x = t
by Th13; ( y = s & Ex (z,p) = q )
Ex (y,z,p) = Ex (s,q)
by A1, Th13;
hence
( y = s & Ex (z,p) = q )
by Th13; verum