Theorem fnmpti 5716

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 2768	. 2 |- A. x e. A B e. _V
3		fnmpti.2	. . 3 |- F = ( x e. A |-> B )
4	3	mptfng 5713	. 2 |- ( A. x e. A B e. _V <-> F Fn A )
5	2, 4	mpbi 213	1 |- F Fn A

Syntax hints:   = wceq 1452   e. wcel 1904   A.wral 2756   _Vcvv 3031   |-> cmpt 4454   Fn wfn 5584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-fun 5591  df-fn 5592

This theorem is referenced by:  dmmpti  5717  fconst  5782  dffn5  5924  eufnfv  6156  idref  6164  offn  6561  caofinvl  6577  fo1st  6832  fo2nd  6833  reldm  6863  mapsnf1o2  7537  unfilem2  7854  fidomdm  7871  pwfilem  7886  noinfep  8183  aceq3lem  8569  dfac4  8571  ackbij2lem2  8688  cfslb2n  8716  axcc2lem  8884  konigthlem  9011  rankcf  9220  tskuni  9226  seqf1o  12292  ccatlen  12772  ccatvalfn  12777  swrdlen  12833  swrdswrd  12870  sqrtf  13503  mptfzshft  13916  fsumrev  13917  fprodrev  14108  efcvgfsum  14217  prmreclem2  14940  1arith  14950  vdwlem6  15015  vdwlem8  15017  slotfn  15213  topnfn  15402  fnmre  15575  cidffn  15662  cidfn  15663  funcres  15879  yonedainv  16244  fn0g  16583  grpinvfn  16784  conjnmz  16994  psgnfn  17220  odf  17264  odfOLD  17280  sylow1lem4  17331  pgpssslw  17344  sylow2blem3  17352  sylow3lem2  17358  cygctb  17604  dprd2da  17753  fnmgp  17803  rlmfn  18491  rrgsupp  18592  asclfn  18637  evlslem1  18815  frlmup4  19436  mdetrlin  19704  fncld  20114  hauseqlcld  20738  kqf  20839  filunirn  20975  fmf  21038  txflf  21099  clsnsg  21202  tgpconcomp  21205  qustgpopn  21212  qustgplem  21213  ustfn  21294  xmetunirn  21430  met1stc  21614  rrxmvallem  22436  ovolf  22513  vitali  22650  i1fmulc  22740  mbfi1fseqlem4  22755  itg2seq  22779  itg2monolem1  22787  i1fibl  22844  fncpn  22966  lhop1lem  23044  mdegxrf  23096  aannenlem3  23365  efabl  23578  logccv  23687  padicabvf  24548  mptelee  25004  wlkiswwlk2lem1  25498  clwlkisclwwlklem2a2  25587  fngid  26023  grpoinvf  26049  occllem  27037  pjfni  27435  pjmfn  27449  rnbra  27841  bra11  27842  kbass2  27851  hmopidmchi  27885  xppreima2  28325  abfmpunirn  28327  dmct  28373  psgnfzto1stlem  28687  fimaproj  28734  locfinreflem  28741  ofcfn  28995  sxbrsigalem3  29167  eulerpartgbij  29278  sseqfv1  29295  sseqfn  29296  sseqf  29298  sseqfv2  29300  signstlen  29528  msubrn  30239  msrf  30252  faclimlem1  30450  poimirlem30  32034  mblfinlem2  32042  volsupnfl  32049  cnambfre  32053  itg2addnclem2  32058  itg2addnclem3  32059  ftc1anclem5  32085  ftc1anclem7  32087  sdclem2  32135  prdsbnd2  32191  rrncmslem  32228  diafn  34673  cdlemm10N  34757  dibfna  34793  lcfrlem9  35189  mapd1o  35287  hdmapfnN  35471  hgmapfnN  35530  rmxypairf1o  35830  hbtlem6  36059  dgraaf  36082  dgraafOLD  36083  cytpfn  36156  uzmptshftfval  36765  binomcxplemrat  36769  addrfn  36895  subrfn  36896  mulvfn  36897  fourierdlem62  38144  fourierdlem70  38152  fourierdlem71  38153  zrinitorngc  40510  zrtermorngc  40511  zrtermoringc  40580