Theorem fnmpti 6022

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

Syntax hints:   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   |-> cmpt 4729   Fn wfn 5883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-fun 5890  df-fn 5891

This theorem is referenced by:  dmmpti  6023  fconst  6091  dffn5  6241  eufnfv  6491  idref  6499  offn  6908  caofinvl  6924  fo1st  7188  fo2nd  7189  reldm  7219  mapsnf1o2  7905  unfilem2  8225  fidomdm  8243  pwfilem  8260  noinfep  8557  aceq3lem  8943  dfac4  8945  ackbij2lem2  9062  cfslb2n  9090  axcc2lem  9258  dmct  9346  konigthlem  9390  rankcf  9599  tskuni  9605  seqf1o  12842  ccatlen  13360  ccatvalfn  13365  swrdlen  13423  swrdswrd  13460  sqrtf  14103  mptfzshft  14510  fsumrev  14511  fprodrev  14707  efcvgfsum  14816  prmreclem2  15621  1arith  15631  vdwlem6  15690  vdwlem8  15692  slotfn  15875  topnfn  16086  fnmre  16251  cidffn  16339  cidfn  16340  funcres  16556  yonedainv  16921  fn0g  17262  grpinvfn  17462  conjnmz  17694  psgnfn  17921  odf  17956  sylow1lem4  18016  pgpssslw  18029  sylow2blem3  18037  sylow3lem2  18043  cygctb  18293  dprd2da  18441  fnmgp  18491  rlmfn  19190  rrgsupp  19291  asclfn  19336  evlslem1  19515  frlmup4  20140  mdetrlin  20408  fncld  20826  hauseqlcld  21449  kqf  21550  filunirn  21686  fmf  21749  txflf  21810  clsnsg  21913  tgpconncomp  21916  qustgpopn  21923  qustgplem  21924  ustfn  22005  xmetunirn  22142  met1stc  22326  rrxmvallem  23187  ovolf  23250  vitali  23382  i1fmulc  23470  mbfi1fseqlem4  23485  itg2seq  23509  itg2monolem1  23517  i1fibl  23574  fncpn  23696  lhop1lem  23776  mdegxrf  23828  aannenlem3  24085  efabl  24296  logccv  24409  gausslemma2dlem1  25091  padicabvf  25320  mptelee  25775  wlkiswwlks2lem1  26755  clwlkclwwlklem2a2  26894  grpoinvf  27386  occllem  28162  pjfni  28560  pjmfn  28574  rnbra  28966  bra11  28967  kbass2  28976  hmopidmchi  29010  xppreima2  29450  abfmpunirn  29452  psgnfzto1stlem  29850  fimaproj  29900  locfinreflem  29907  ofcfn  30162  sxbrsigalem3  30334  eulerpartgbij  30434  sseqfv1  30451  sseqfn  30452  sseqf  30454  sseqfv2  30456  signstlen  30644  msubrn  31426  msrf  31439  faclimlem1  31629  bj-evalfn  33026  matunitlindflem1  33405  poimirlem30  33439  mblfinlem2  33447  volsupnfl  33454  cnambfre  33458  itg2addnclem2  33462  itg2addnclem3  33463  ftc1anclem5  33489  ftc1anclem7  33491  sdclem2  33538  prdsbnd2  33594  rrncmslem  33631  diafn  36323  cdlemm10N  36407  dibfna  36443  lcfrlem9  36839  mapd1o  36937  hdmapfnN  37121  hgmapfnN  37180  rmxypairf1o  37476  hbtlem6  37699  dgraaf  37717  cytpfn  37786  ntrf  38421  uzmptshftfval  38545  binomcxplemrat  38549  addrfn  38676  subrfn  38677  mulvfn  38678  limsup10exlem  40004  liminfvalxr  40015  fourierdlem62  40385  fourierdlem70  40393  fourierdlem71  40394  fmtnorn  41446  zrinitorngc  42000  zrtermorngc  42001  zrtermoringc  42070