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 2818	. 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 208	1 |- F Fn A

Syntax hints:   = wceq 1395   e. wcel 1819   A.wral 2807   _Vcvv 3109   |-> cmpt 4515   Fn wfn 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-fun 5596  df-fn 5597

This theorem is referenced by:  dmmpti  5716  fconst  5777  dffn5  5918  eufnfv  6147  idref  6154  offn  6550  caofinvl  6566  fo1st  6819  fo2nd  6820  reldm  6850  mapsnf1o2  7485  unfilem2  7803  fidomdm  7820  pwfilem  7832  noinfep  8093  aceq3lem  8518  dfac4  8520  ackbij2lem2  8637  cfslb2n  8665  axcc2lem  8833  konigthlem  8960  rankcf  9172  tskuni  9178  seqf1o  12151  ccatlen  12603  ccatvalfn  12608  swrdlen  12659  swrdswrd  12697  sqrtf  13208  mptfzshft  13605  fsumrev  13606  fprodrev  13793  efcvgfsum  13833  prmreclem2  14447  1arith  14457  vdwlem6  14516  vdwlem8  14518  slotfn  14658  topnfn  14843  fnmre  15008  cidffn  15095  cidfn  15096  funcres  15312  yonedainv  15677  fn0g  16016  grpinvfn  16217  conjnmz  16427  psgnfn  16653  odf  16688  sylow1lem4  16748  pgpssslw  16761  sylow2blem3  16769  sylow3lem2  16775  cygctb  17021  dprd2da  17218  fnmgp  17270  rlmfn  17963  rrgsupp  18066  asclfn  18112  evlslem1  18311  frlmup4  18962  mdetrlin  19231  fncld  19650  hauseqlcld  20273  kqf  20374  filunirn  20509  fmf  20572  txflf  20633  clsnsg  20734  tgpconcomp  20737  qustgpopn  20744  qustgplem  20745  ustfn  20830  xmetunirn  20966  met1stc  21150  rrxmvallem  21957  ovolf  22019  vitali  22148  i1fmulc  22236  mbfi1fseqlem4  22251  itg2seq  22275  itg2monolem1  22283  i1fibl  22340  fncpn  22462  lhop1lem  22540  mdegxrf  22594  aannenlem3  22852  efabl  23063  logccv  23170  padicabvf  23942  mptelee  24325  wlkiswwlk2lem1  24818  clwlkisclwwlklem2a2  24907  fngid  25343  grpoinvf  25369  occllem  26348  pjfni  26746  pjmfn  26760  rnbra  27153  bra11  27154  kbass2  27163  hmopidmchi  27197  xppreima2  27636  abfmpunirn  27638  dmct  27694  fimaproj  27997  locfinreflem  28004  ofcfn  28272  sxbrsigalem3  28416  eulerpartgbij  28508  sseqfv1  28525  sseqfn  28526  sseqf  28528  sseqfv2  28530  signstlen  28721  msubrn  29086  msrf  29099  faclimlem1  29386  mblfinlem2  30257  volsupnfl  30264  cnambfre  30268  itg2addnclem2  30272  itg2addnclem3  30273  ftc1anclem5  30299  ftc1anclem7  30301  sdclem2  30440  prdsbnd2  30496  rrncmslem  30533  rmxypairf1o  31051  hbtlem6  31282  dgraaf  31300  cytpfn  31372  uzmptshftfval  31455  binomcxplemrat  31459  addrfn  31585  subrfn  31586  mulvfn  31587  fourierdlem62  32154  fourierdlem70  32162  fourierdlem71  32163  zrinitorngc  32952  zrtermorngc  32953  zrtermoringc  33022  diafn  36904  cdlemm10N  36988  dibfna  37024  lcfrlem9  37420  mapd1o  37518  hdmapfnN  37702  hgmapfnN  37761