let A be QC-alphabet ; for x, y being bound_QC-variable of A
for p, q being Element of QC-WFF A st Ex (x,p) = Ex (y,q) holds
( x = y & p = q )
let x, y be bound_QC-variable of A; for p, q being Element of QC-WFF A st Ex (x,p) = Ex (y,q) holds
( x = y & p = q )
let p, q be Element of QC-WFF A; ( Ex (x,p) = Ex (y,q) implies ( x = y & p = q ) )
assume
Ex (x,p) = Ex (y,q)
; ( x = y & p = q )
then A1:
All (x,('not' p)) = All (y,('not' q))
by FINSEQ_1:33;
then
'not' p = 'not' q
by Th5;
hence
( x = y & p = q )
by A1, Th5, FINSEQ_1:33; verum