MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nff Structured version   Visualization version   GIF version

Theorem nff 6726
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
StepHypRef Expression
1 df-f 6560 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
2 nff.1 . . . 4 𝑥𝐹
3 nff.2 . . . 4 𝑥𝐴
42, 3nffn 6661 . . 3 𝑥 𝐹 Fn 𝐴
52nfrn 5960 . . . 4 𝑥ran 𝐹
6 nff.3 . . . 4 𝑥𝐵
75, 6nfss 3972 . . 3 𝑥ran 𝐹𝐵
84, 7nfan 1895 . 2 𝑥(𝐹 Fn 𝐴 ∧ ran 𝐹𝐵)
91, 8nfxfr 1848 1 𝑥 𝐹:𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wa 394  wnf 1778  wnfc 2876  wss 3947  ran crn 5685   Fn wfn 6551  wf 6552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-br 5156  df-opab 5218  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-fun 6558  df-fn 6559  df-f 6560
This theorem is referenced by:  nff1  6798  dffo3f  7122  nfwrd  14553  lfgrnloop  29064  fcomptf  32577  aciunf1lem  32581  fnpreimac  32590  esumfzf  33904  esumfsup  33905  poimirlem24  37347  sdclem1  37446  fmuldfeqlem1  45221  fnlimfvre  45313  dvnmul  45582  stoweidlem53  45692  stoweidlem54  45693  stoweidlem57  45696  sge0iunmpt  46057
  Copyright terms: Public domain W3C validator