Theorem elopt | index | src |

theorem elopt (A: set) (a: nat): $ a e. Option A <-> a = 0 \/ a - 1 e. A $;
StepHypRefExpression
1 eqeq1
n = a -> (n = 0 <-> a = 0)
2 subeq1
n = a -> n - 1 = a - 1
3 2 eleq1d
n = a -> (n - 1 e. A <-> a - 1 e. A)
4 1, 3 oreqd
n = a -> (n = 0 \/ n - 1 e. A <-> a = 0 \/ a - 1 e. A)
5 4 elabe
a e. {n | n = 0 \/ n - 1 e. A} <-> a = 0 \/ a - 1 e. A
6 5 conv Option
a e. Option A <-> a = 0 \/ a - 1 e. A

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (addeq)