Theorem nfisf | index | src |

theorem nfisf {x: nat} (F: set x): $ FS/ x F $ > $ F/ x isfun F $;
StepHypRefExpression
1 hyp hF
FS/ x F
2 1 nfel2
F/ x a1, a2 e. F
3 1 nfel2
F/ x a1, a3 e. F
4 nfv
F/ x a2 = a3
5 3, 4 nfim
F/ x a1, a3 e. F -> a2 = a3
6 2, 5 nfim
F/ x a1, a2 e. F -> a1, a3 e. F -> a2 = a3
7 6 nfal
F/ x A. a3 (a1, a2 e. F -> a1, a3 e. F -> a2 = a3)
8 7 nfal
F/ x A. a2 A. a3 (a1, a2 e. F -> a1, a3 e. F -> a2 = a3)
9 8 nfal
F/ x A. a1 A. a2 A. a3 (a1, a2 e. F -> a1, a3 e. F -> a2 = a3)
10 9 conv isfun
F/ x isfun F

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (ax_8)