Theorem nffunc | index | src |

theorem nffunc {x: nat} (F A B: set x):
  $ FS/ x F $ >
  $ FS/ x A $ >
  $ FS/ x B $ >
  $ F/ x func F A B $;
StepHypRefExpression
1 hyp hF
FS/ x F
2 1 nfisf
F/ x isfun F
3 1 nfdm
FS/ x Dom F
4 hyp hA
FS/ x A
5 3, 4 nfeqs
F/ x Dom F == A
6 2, 5 nfan
F/ x isfun F /\ Dom F == A
7 1 nfrn
FS/ x Ran F
8 hyp hB
FS/ x B
9 7, 8 nfss
F/ x Ran F C_ B
10 6, 9 nfan
F/ x isfun F /\ Dom F == A /\ Ran F C_ B
11 10 conv func
F/ x func F A 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_set (elab, ax_8)