theorem :: ZF_LANG1:183

for H being ZF-formula
for x being Variable holds H / (x,x) = H