Theorem eqallt1 ≪ | index | src | ≫ 

theorem eqallt1 (a b: nat) {i: nat}: $ a = b <-> A. i (i < a <-> i < b) $;
StepHypRefExpression
1 bitr 
(a = b <-> A. i (a <= i <-> b <= i)) -> (A. i (a <= i <-> b <= i) <-> A. i (i < a <-> i < b)) -> (a = b <-> A. i (i < a <-> i < b))
2 eqalle2 
a = b <-> A. i (a <= i <-> b <= i)
3 1, 2 ax_mp 
(A. i (a <= i <-> b <= i) <-> A. i (i < a <-> i < b)) -> (a = b <-> A. i (i < a <-> i < b))
4 bitr4 
(a <= i <-> b <= i <-> (~a <= i <-> ~b <= i)) -> (i < a <-> i < b <-> (~a <= i <-> ~b <= i)) -> (a <= i <-> b <= i <-> (i < a <-> i < b))
5 con3bb 
a <= i <-> b <= i <-> (~a <= i <-> ~b <= i)
6 4, 5 ax_mp 
(i < a <-> i < b <-> (~a <= i <-> ~b <= i)) -> (a <= i <-> b <= i <-> (i < a <-> i < b))
7 bieq 
(i < a <-> ~a <= i) -> (i < b <-> ~b <= i) -> (i < a <-> i < b <-> (~a <= i <-> ~b <= i))
8 ltnle 
i < a <-> ~a <= i
9 7, 8 ax_mp 
(i < b <-> ~b <= i) -> (i < a <-> i < b <-> (~a <= i <-> ~b <= i))
10 ltnle 
i < b <-> ~b <= i
11 9, 10 ax_mp 
i < a <-> i < b <-> (~a <= i <-> ~b <= i)
12 6, 11 ax_mp 
a <= i <-> b <= i <-> (i < a <-> i < b)
13 12 aleqi 
A. i (a <= i <-> b <= i) <-> A. i (i < a <-> i < b)
14 3, 13 ax_mp 
a = b <-> A. i (i < a <-> i < b)

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_peano (peano1, peano2, peano5, addeq, add0, addS)