theorem ocasep0 (S: set) (z: wff): $ 0 e. ocasep z S <-> z $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifppos | a1 = 0 -> (ifp (a1 = 0) z (a1 - 1 e. S) <-> z) |
|
2 | 1 | elabe | 0 e. {a1 | ifp (a1 = 0) z (a1 - 1 e. S)} <-> z |
3 | 2 | conv ocasep | 0 e. ocasep z S <-> z |