theorem :: QC_LANG2:16

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 All (x,y,p) = All (z,q) holds
( x = z & All (y,p) = q ) by Th5;