Theorem fnmpti 5715

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

Syntax hints:   = wceq 1437   e. wcel 1867   A.wral 2773   _Vcvv 3078   |-> cmpt 4475   Fn wfn 5587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-br 4418  df-opab 4476  df-mpt 4477  df-id 4760  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-fun 5594  df-fn 5595

This theorem is referenced by:  dmmpti  5716  fconst  5777  dffn5  5917  eufnfv  6145  idref  6152  offn  6547  caofinvl  6563  fo1st  6818  fo2nd  6819  reldm  6849  mapsnf1o2  7518  unfilem2  7833  fidomdm  7850  pwfilem  7865  noinfep  8155  aceq3lem  8540  dfac4  8542  ackbij2lem2  8659  cfslb2n  8687  axcc2lem  8855  konigthlem  8982  rankcf  9191  tskuni  9197  seqf1o  12240  ccatlen  12697  ccatvalfn  12702  swrdlen  12753  swrdswrd  12790  sqrtf  13394  mptfzshft  13806  fsumrev  13807  fprodrev  13998  efcvgfsum  14107  prmreclem2  14813  1arith  14823  vdwlem6  14888  vdwlem8  14890  slotfn  15087  topnfn  15276  fnmre  15441  cidffn  15528  cidfn  15529  funcres  15745  yonedainv  16110  fn0g  16449  grpinvfn  16650  conjnmz  16860  psgnfn  17086  odf  17121  sylow1lem4  17181  pgpssslw  17194  sylow2blem3  17202  sylow3lem2  17208  cygctb  17454  dprd2da  17603  fnmgp  17653  rlmfn  18341  rrgsupp  18443  asclfn  18488  evlslem1  18666  frlmup4  19283  mdetrlin  19551  fncld  19961  hauseqlcld  20585  kqf  20686  filunirn  20821  fmf  20884  txflf  20945  clsnsg  21048  tgpconcomp  21051  qustgpopn  21058  qustgplem  21059  ustfn  21140  xmetunirn  21276  met1stc  21460  rrxmvallem  22244  ovolf  22309  vitali  22445  i1fmulc  22535  mbfi1fseqlem4  22550  itg2seq  22574  itg2monolem1  22582  i1fibl  22639  fncpn  22761  lhop1lem  22839  mdegxrf  22891  aannenlem3  23148  efabl  23361  logccv  23470  padicabvf  24329  mptelee  24768  wlkiswwlk2lem1  25261  clwlkisclwwlklem2a2  25350  fngid  25784  grpoinvf  25810  occllem  26788  pjfni  27186  pjmfn  27200  rnbra  27592  bra11  27593  kbass2  27602  hmopidmchi  27636  xppreima2  28086  abfmpunirn  28088  dmct  28138  psgnfzto1stlem  28449  fimaproj  28496  locfinreflem  28503  ofcfn  28757  sxbrsigalem3  28930  eulerpartgbij  29028  sseqfv1  29045  sseqfn  29046  sseqf  29048  sseqfv2  29050  signstlen  29241  msubrn  29952  msrf  29965  faclimlem1  30163  poimirlem30  31674  mblfinlem2  31682  volsupnfl  31689  cnambfre  31693  itg2addnclem2  31698  itg2addnclem3  31699  ftc1anclem5  31725  ftc1anclem7  31727  sdclem2  31775  prdsbnd2  31831  rrncmslem  31868  diafn  34311  cdlemm10N  34395  dibfna  34431  lcfrlem9  34827  mapd1o  34925  hdmapfnN  35109  hgmapfnN  35168  rmxypairf1o  35469  hbtlem6  35698  dgraaf  35716  cytpfn  35788  uzmptshftfval  36336  binomcxplemrat  36340  addrfn  36466  subrfn  36467  mulvfn  36468  fourierdlem62  37604  fourierdlem70  37612  fourierdlem71  37613  zrinitorngc  38773  zrtermorngc  38774  zrtermoringc  38843