Theorem fnmpti 5706

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

Syntax hints:   = wceq 1444   e. wcel 1887   A.wral 2737   _Vcvv 3045   |-> cmpt 4461   Fn wfn 5577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-fun 5584  df-fn 5585

This theorem is referenced by:  dmmpti  5707  fconst  5769  dffn5  5910  eufnfv  6139  idref  6146  offn  6542  caofinvl  6558  fo1st  6813  fo2nd  6814  reldm  6844  mapsnf1o2  7519  unfilem2  7836  fidomdm  7853  pwfilem  7868  noinfep  8165  aceq3lem  8551  dfac4  8553  ackbij2lem2  8670  cfslb2n  8698  axcc2lem  8866  konigthlem  8993  rankcf  9202  tskuni  9208  seqf1o  12254  ccatlen  12721  ccatvalfn  12726  swrdlen  12779  swrdswrd  12816  sqrtf  13426  mptfzshft  13839  fsumrev  13840  fprodrev  14031  efcvgfsum  14140  prmreclem2  14861  1arith  14871  vdwlem6  14936  vdwlem8  14938  slotfn  15135  topnfn  15324  fnmre  15497  cidffn  15584  cidfn  15585  funcres  15801  yonedainv  16166  fn0g  16505  grpinvfn  16706  conjnmz  16916  psgnfn  17142  odf  17186  odfOLD  17202  sylow1lem4  17253  pgpssslw  17266  sylow2blem3  17274  sylow3lem2  17280  cygctb  17526  dprd2da  17675  fnmgp  17725  rlmfn  18413  rrgsupp  18515  asclfn  18560  evlslem1  18738  frlmup4  19359  mdetrlin  19627  fncld  20037  hauseqlcld  20661  kqf  20762  filunirn  20897  fmf  20960  txflf  21021  clsnsg  21124  tgpconcomp  21127  qustgpopn  21134  qustgplem  21135  ustfn  21216  xmetunirn  21352  met1stc  21536  rrxmvallem  22358  ovolf  22435  vitali  22571  i1fmulc  22661  mbfi1fseqlem4  22676  itg2seq  22700  itg2monolem1  22708  i1fibl  22765  fncpn  22887  lhop1lem  22965  mdegxrf  23017  aannenlem3  23286  efabl  23499  logccv  23608  padicabvf  24469  mptelee  24925  wlkiswwlk2lem1  25419  clwlkisclwwlklem2a2  25508  fngid  25942  grpoinvf  25968  occllem  26956  pjfni  27354  pjmfn  27368  rnbra  27760  bra11  27761  kbass2  27770  hmopidmchi  27804  xppreima2  28249  abfmpunirn  28251  dmct  28298  psgnfzto1stlem  28613  fimaproj  28660  locfinreflem  28667  ofcfn  28921  sxbrsigalem3  29094  eulerpartgbij  29205  sseqfv1  29222  sseqfn  29223  sseqf  29225  sseqfv2  29227  signstlen  29456  msubrn  30167  msrf  30180  faclimlem1  30379  poimirlem30  31970  mblfinlem2  31978  volsupnfl  31985  cnambfre  31989  itg2addnclem2  31994  itg2addnclem3  31995  ftc1anclem5  32021  ftc1anclem7  32023  sdclem2  32071  prdsbnd2  32127  rrncmslem  32164  diafn  34602  cdlemm10N  34686  dibfna  34722  lcfrlem9  35118  mapd1o  35216  hdmapfnN  35400  hgmapfnN  35459  rmxypairf1o  35759  hbtlem6  35988  dgraaf  36011  dgraafOLD  36012  cytpfn  36085  uzmptshftfval  36695  binomcxplemrat  36699  addrfn  36825  subrfn  36826  mulvfn  36827  fourierdlem62  38032  fourierdlem70  38040  fourierdlem71  38041  zrinitorngc  40055  zrtermorngc  40056  zrtermoringc  40125