theorem ocasepeq2d (_G z: wff) (_S1 _S2: set): $ _G -> _S1 == _S2 $ > $ _G -> ocasep z _S1 == ocasep z _S2 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biidd | _G -> (z <-> z) |
|
2 | hyp _h | _G -> _S1 == _S2 |
|
3 | 1, 2 | ocasepeqd | _G -> ocasep z _S1 == ocasep z _S2 |