Theorem excons ≪ | index | src | ≫ 

theorem excons (a: nat) {x y: nat}: $ a != 0 <-> E. x E. y a = x : y $;
StepHypRefExpression
1 consfstsnd 
a != 0 -> fst (a - 1) : snd (a - 1) = a
2 anll 
fst (a - 1) : snd (a - 1) = a /\ x = fst (a - 1) /\ y = snd (a - 1) -> fst (a - 1) : snd (a - 1) = a
3 anlr 
fst (a - 1) : snd (a - 1) = a /\ x = fst (a - 1) /\ y = snd (a - 1) -> x = fst (a - 1)
4 anr 
fst (a - 1) : snd (a - 1) = a /\ x = fst (a - 1) /\ y = snd (a - 1) -> y = snd (a - 1)
5 3, 4 conseqd 
fst (a - 1) : snd (a - 1) = a /\ x = fst (a - 1) /\ y = snd (a - 1) -> x : y = fst (a - 1) : snd (a - 1)
6 5 eqcomd 
fst (a - 1) : snd (a - 1) = a /\ x = fst (a - 1) /\ y = snd (a - 1) -> fst (a - 1) : snd (a - 1) = x : y
7 2, 6 eqtr3d 
fst (a - 1) : snd (a - 1) = a /\ x = fst (a - 1) /\ y = snd (a - 1) -> a = x : y
8 7 iexde 
fst (a - 1) : snd (a - 1) = a /\ x = fst (a - 1) -> E. y a = x : y
9 8 iexde 
fst (a - 1) : snd (a - 1) = a -> E. x E. y a = x : y
10 1, 9 rsyl 
a != 0 -> E. x E. y a = x : y
11 consne0 
x : y != 0
12 neeq1 
a = x : y -> (a != 0 <-> x : y != 0)
13 11, 12 mpbiri 
a = x : y -> a != 0
14 13 eex 
E. y a = x : y -> a != 0
15 14 eex 
E. x E. y a = x : y -> a != 0
16 10, 15 ibii 
a != 0 <-> E. x E. y a = x : y

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, peano5, addeq, muleq, add0, addS, mul0, mulS)