Theorem theo0 | index | src |

theorem theo0 {x y: nat} (A: set): $ ~E. y A == {x | x = y} <-> theo A = 0 $;
StepHypRefExpression
1 theo01
~E. y A == {x | x = y} -> theo A = 0
2 con2
(E. y A == {x | x = y} -> ~theo A = 0) -> theo A = 0 -> ~E. y A == {x | x = y}
3 sucne0
theo A = suc y -> theo A != 0
4 3 conv ne
theo A = suc y -> ~theo A = 0
5 theoid1
A == {x | x = y} -> theo A = suc y
6 4, 5 syl
A == {x | x = y} -> ~theo A = 0
7 6 eex
E. y A == {x | x = y} -> ~theo A = 0
8 2, 7 ax_mp
theo A = 0 -> ~E. y A == {x | x = y}
9 1, 8 ibii
~E. y A == {x | x = y} <-> theo A = 0

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 (peano1, peano2)