theorem :: ZF_LANG1:21

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