Theorem nff 6710

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 6547	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		nff.1	. . . 4 ⊢ Ⅎ𝑥𝐹
3		nff.2	. . . 4 ⊢ Ⅎ𝑥𝐴
4	2, 3	nffn 6643	. . 3 ⊢ Ⅎ𝑥 𝐹 Fn 𝐴
5	2	nfrn 5935	. . . 4 ⊢ Ⅎ𝑥ran 𝐹
6		nff.3	. . . 4 ⊢ Ⅎ𝑥𝐵
7	5, 6	nfss 3902	. . 3 ⊢ Ⅎ𝑥ran 𝐹 ⊆ 𝐵
8	4, 7	nfan 1931	. 2 ⊢ Ⅎ𝑥(𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	1, 8	nfxfr 1885	1 ⊢ Ⅎ𝑥 𝐹:𝐴⟶𝐵

This proof depends on syntax axioms:   ∧ wa 401  Ⅎwnf 1815  Ⅎwnfc 2907   ⊆ wss 3896  ran crn 5652   Fn wfn 6538  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6545  df-fn 6546  df-f 6547

This theorem is used by:  nff1  6781  dffo3f  7111  nfwrd  14695  lfgrnloop  29712  fcomptf  33303  aciunf1lem  33307  fnpreimac  33315  esumfzf  34751  esumfsup  34752  poimirlem24  38699  sdclem1  38814  nfrelp  46075  fmuldfeqlem1  46730  fnlimfvre  46820  dvnmul  47089  stoweidlem53  47199  stoweidlem54  47200  stoweidlem57  47203  sge0iunmpt  47564