Theorem fnmpti 5527

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)

Hypotheses

Ref	Expression
fnmpti.1	|- B e. _V
fnmpti.2	|- F = ( x e. A |-> B )

Assertion

Ref	Expression
fnmpti	|- F Fn A

Distinct variable group:   x, A

Allowed substitution hints:   B( x)   F( x)

Proof of Theorem fnmpti

Step	Hyp	Ref	Expression
1		fnmpti.1	. . 3 |- B e. _V
2	1	rgenw 2773	. 2 |- A. x e. A B e. _V
3		fnmpti.2	. . 3 |- F = ( x e. A |-> B )
4	3	mptfng 5524	. 2 |- ( A. x e. A B e. _V <-> F Fn A )
5	2, 4	mpbi 208	1 |- F Fn A

Syntax hints:   = wceq 1362   e. wcel 1755   A.wral 2705   _Vcvv 2962   e. cmpt 4338   Fn wfn 5401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-fun 5408  df-fn 5409

This theorem is referenced by:  dmmpti  5528  fconst  5584  dffn5  5725  eufnfv  5938  idref  5945  offn  6320  caofinvl  6336  fo1st  6585  fo2nd  6586  reldm  6614  mapsnf1o2  7248  unfilem2  7565  fidomdm  7581  pwfilem  7593  noinfep  7853  aceq3lem  8278  dfac4  8280  ackbij2lem2  8397  cfslb2n  8425  axcc2lem  8593  konigthlem  8720  rankcf  8931  tskuni  8937  seqf1o  11830  ccatlen  12258  ccatvalfn  12263  swrdlen  12302  swrdvalfn  12315  swrdswrd  12337  sqrf  12834  fsumrev  13228  fsumshft  13229  efcvgfsum  13353  prmreclem2  13960  1arith  13970  vdwlem6  14029  vdwlem8  14031  slotfn  14170  topnfn  14346  fnmre  14511  cidffn  14598  cidfn  14599  funcres  14788  yonedainv  15073  fn0g  15415  grpinvfn  15557  conjnmz  15759  psgnfn  15986  odf  16019  sylow1lem4  16079  pgpssslw  16092  sylow2blem3  16100  sylow3lem2  16106  cygctb  16347  dprd2da  16514  fnmgp  16566  rlmfn  17192  rrgsupp  17283  asclfn  17328  frlmup4  18070  mdetrlin  18250  fncld  18467  hauseqlcld  19060  kqf  19161  filunirn  19296  fmf  19359  txflf  19420  clsnsg  19521  tgpconcomp  19524  divstgpopn  19531  divstgplem  19532  ustfn  19617  xmetunirn  19753  met1stc  19937  rrxmvallem  20744  ovolf  20806  vitali  20934  i1fmulc  21022  mbfi1fseqlem4  21037  itg2seq  21061  itg2monolem1  21069  i1fibl  21126  fncpn  21248  lhop1lem  21326  evlslem1  21366  mdegxrf  21423  aannenlem3  21680  logccv  21992  padicabvf  22764  mptelee  22963  fngid  23523  grpoinvf  23549  occllem  24528  pjfni  24926  pjmfn  24940  rnbra  25333  bra11  25334  kbass2  25343  hmopidmchi  25377  xppreima2  25788  abfmpunirn  25790  dmct  25837  ofcfn  26395  sxbrsigalem3  26540  eulerpartgbij  26602  sseqfv1  26619  sseqfn  26620  sseqf  26622  sseqfv2  26624  fprodshft  27333  fprodrev  27334  faclimlem1  27395  mblfinlem2  28270  volsupnfl  28277  cnambfre  28281  itg2addnclem2  28285  itg2addnclem3  28286  ftc1anclem5  28312  ftc1anclem7  28314  sdclem2  28479  prdsbnd2  28535  rrncmslem  28572  rmxypairf1o  29094  hbtlem6  29327  dgraaf  29346  cytpfn  29418  addrfn  29570  subrfn  29571  mulvfn  29572  wlkiswwlk2lem1  30168  clwlkisclwwlklem2a2  30285  diafn  34249  cdlemm10N  34333  dibfna  34369  lcfrlem9  34765  mapd1o  34863  hdmapfnN  35047  hgmapfnN  35106