theorem imaeq1d (_G: wff) (_F1 _F2 A: set): $ _G -> _F1 == _F2 $ > $ _G -> _F1 '' A == _F2 '' A $;
_G -> _F1 == _F2
_G -> A == A
_G -> _F1 '' A == _F2 '' A