theorem :: ZF_FUND1:22

for V being Universe
for X being Subclass of V
for E being non empty set
for H being ZF-formula st X is closed_wrt_A1-A7 & E in X holds
Diagram (H,E) in X