theorem :: QC_LANG2:18

for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A st Ex (x,y,p) = Ex (z,q) holds
( x = z & Ex (y,p) = q ) by Th13;