theorem :: ZF_LANG1:11

for p being ZF-formula
for x, y being Variable holds
( All (x,y,p) is universal & bound_in (All (x,y,p)) = x & the_scope_of (All (x,y,p)) = All (y,p) ) by Th8;