Theorem nff 6656

Description: Bound-variable hypothesis builder for a mapping. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)

Hypotheses

Ref	Expression
nff.1	⊢ Ⅎ𝑥𝐹
nff.2	⊢ Ⅎ𝑥𝐴
nff.3	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nff	⊢ Ⅎ𝑥 𝐹:𝐴⟶𝐵

Proof of Theorem nff

Step	Hyp	Ref	Expression
1		df-f 6494	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		nff.1	. . . 4 ⊢ Ⅎ𝑥𝐹
3		nff.2	. . . 4 ⊢ Ⅎ𝑥𝐴
4	2, 3	nffn 6589	. . 3 ⊢ Ⅎ𝑥 𝐹 Fn 𝐴
5	2	nfrn 5899	. . . 4 ⊢ Ⅎ𝑥ran 𝐹
6		nff.3	. . . 4 ⊢ Ⅎ𝑥𝐵
7	5, 6	nfss 3924	. . 3 ⊢ Ⅎ𝑥ran 𝐹 ⊆ 𝐵
8	4, 7	nfan 1900	. 2 ⊢ Ⅎ𝑥(𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	1, 8	nfxfr 1854	1 ⊢ Ⅎ𝑥 𝐹:𝐴⟶𝐵

Syntax hints:   ∧ wa 395  Ⅎwnf 1784  Ⅎwnfc 2881   ⊆ wss 3899  ran crn 5623   Fn wfn 6485  ⟶wf 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ral 3050  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-fun 6492  df-fn 6493  df-f 6494

This theorem is referenced by:  nff1  6726  dffo3f  7049  nfwrd  14464  lfgrnloop  29147  fcomptf  32685  aciunf1lem  32689  fnpreimac  32698  esumfzf  34175  esumfsup  34176  poimirlem24  37784  sdclem1  37883  nfrelp  45132  fmuldfeqlem1  45770  fnlimfvre  45860  dvnmul  46129  stoweidlem53  46239  stoweidlem54  46240  stoweidlem57  46243  sge0iunmpt  46604