Theorem srecpval | index | src |

pub theorem srecpval {i: nat} (A: set) (n: nat):
  $ srecp A n <-> n, sep (upto n) {i | srecp A i} e. A $;
StepHypRefExpression
1 bitr
(srecp A n <-> true (nat (n, sep (upto n) {i | srecp A i} e. A))) ->
  (true (nat (n, sep (upto n) {i | srecp A i} e. A)) <-> n, sep (upto n) {i | srecp A i} e. A) ->
  (srecp A n <-> n, sep (upto n) {i | srecp A i} e. A)
2 trueeq
srecpaux A n = nat (n, sep (upto n) {i | srecp A i} e. A) -> (true (srecpaux A n) <-> true (nat (n, sep (upto n) {i | srecp A i} e. A)))
3 2 conv srecp
srecpaux A n = nat (n, sep (upto n) {i | srecp A i} e. A) -> (srecp A n <-> true (nat (n, sep (upto n) {i | srecp A i} e. A)))
4 srecpauxval
srecpaux A n = nat (n, sep (upto n) {i | srecp A i} e. A)
5 3, 4 ax_mp
srecp A n <-> true (nat (n, sep (upto n) {i | srecp A i} e. A))
6 1, 5 ax_mp
(true (nat (n, sep (upto n) {i | srecp A i} e. A)) <-> n, sep (upto n) {i | srecp A i} e. A) -> (srecp A n <-> n, sep (upto n) {i | srecp A i} e. A)
7 truenat
true (nat (n, sep (upto n) {i | srecp A i} e. A)) <-> n, sep (upto n) {i | srecp A i} e. A
8 6, 7 ax_mp
srecp A n <-> n, sep (upto n) {i | srecp A i} 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 (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)