Theorem pseteqd ≪ | index | src | ≫ 

theorem pseteqd (_G: wff) (_a1 _a2: nat):
  $ _G -> _a1 = _a2 $ >
  $ _G -> pset _a1 == pset _a2 $;
StepHypRefExpression
1 eqidd 
_G -> 0 = 0
2 hyp _ah 
_G -> _a1 = _a2
3 2 fsteqd 
_G -> fst _a1 = fst _a2
4 1, 3 lteqd 
_G -> (0 < fst _a1 <-> 0 < fst _a2)
5 2 sndeqd 
_G -> snd _a1 = snd _a2
6 1, 5 lteqd 
_G -> (0 < snd _a1 <-> 0 < snd _a2)
7 4, 6 aneqd 
_G -> (0 < fst _a1 /\ 0 < snd _a1 <-> 0 < fst _a2 /\ 0 < snd _a2)
8 biidd 
_G -> (0 < x /\ x <= n <-> 0 < x /\ x <= n)
9 eqidd 
_G -> x = x
10 9, 3 dvdeqd 
_G -> (x || fst _a1 <-> x || fst _a2)
11 8, 10 imeqd 
_G -> (0 < x /\ x <= n -> x || fst _a1 <-> 0 < x /\ x <= n -> x || fst _a2)
12 11 aleqd 
_G -> (A. x (0 < x /\ x <= n -> x || fst _a1) <-> A. x (0 < x /\ x <= n -> x || fst _a2))
13 7, 12 aneqd 
_G -> (0 < fst _a1 /\ 0 < snd _a1 /\ A. x (0 < x /\ x <= n -> x || fst _a1) <-> 0 < fst _a2 /\ 0 < snd _a2 /\ A. x (0 < x /\ x <= n -> x || fst _a2))
14 eqidd 
_G -> suc n = suc n
15 3, 14 muleqd 
_G -> fst _a1 * suc n = fst _a2 * suc n
16 15 suceqd 
_G -> suc (fst _a1 * suc n) = suc (fst _a2 * suc n)
17 16, 5 dvdeqd 
_G -> (suc (fst _a1 * suc n) || snd _a1 <-> suc (fst _a2 * suc n) || snd _a2)
18 13, 17 aneqd 
_G ->
  (0 < fst _a1 /\ 0 < snd _a1 /\ A. x (0 < x /\ x <= n -> x || fst _a1) /\ suc (fst _a1 * suc n) || snd _a1 <->
    0 < fst _a2 /\ 0 < snd _a2 /\ A. x (0 < x /\ x <= n -> x || fst _a2) /\ suc (fst _a2 * suc n) || snd _a2)
19 18 abeqd 
_G ->
  {n | 0 < fst _a1 /\ 0 < snd _a1 /\ A. x (0 < x /\ x <= n -> x || fst _a1) /\ suc (fst _a1 * suc n) || snd _a1} ==
    {n | 0 < fst _a2 /\ 0 < snd _a2 /\ A. x (0 < x /\ x <= n -> x || fst _a2) /\ suc (fst _a2 * suc n) || snd _a2}
20 19 conv pset 
_G -> pset _a1 == pset _a2

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