Theorem fnmpti 5642

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

Syntax hints:   = wceq 1370   e. wcel 1758   A.wral 2796   _Vcvv 3072   |-> cmpt 4453   Fn wfn 5516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431  ax-sep 4516  ax-nul 4524  ax-pr 4634

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2265  df-mo 2266  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-ne 2647  df-ral 2801  df-rex 2802  df-rab 2805  df-v 3074  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-nul 3741  df-if 3895  df-sn 3981  df-pr 3983  df-op 3987  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4739  df-xp 4949  df-rel 4950  df-cnv 4951  df-co 4952  df-dm 4953  df-fun 5523  df-fn 5524

This theorem is referenced by:  dmmpti  5643  fconst  5699  dffn5  5841  eufnfv  6055  idref  6062  offn  6436  caofinvl  6452  fo1st  6701  fo2nd  6702  reldm  6730  mapsnf1o2  7365  unfilem2  7683  fidomdm  7699  pwfilem  7711  noinfep  7971  aceq3lem  8396  dfac4  8398  ackbij2lem2  8515  cfslb2n  8543  axcc2lem  8711  konigthlem  8838  rankcf  9050  tskuni  9056  seqf1o  11959  ccatlen  12388  ccatvalfn  12393  swrdlen  12432  swrdvalfn  12445  swrdswrd  12467  sqrf  12964  mptfzshft  13358  fsumrev  13359  efcvgfsum  13484  prmreclem2  14091  1arith  14101  vdwlem6  14160  vdwlem8  14162  slotfn  14301  topnfn  14478  fnmre  14643  cidffn  14730  cidfn  14731  funcres  14920  yonedainv  15205  fn0g  15547  grpinvfn  15692  conjnmz  15894  psgnfn  16121  odf  16156  sylow1lem4  16216  pgpssslw  16229  sylow2blem3  16237  sylow3lem2  16243  cygctb  16484  dprd2da  16658  fnmgp  16710  rlmfn  17389  rrgsupp  17480  asclfn  17525  evlslem1  17720  frlmup4  18349  mdetrlin  18535  fncld  18753  hauseqlcld  19346  kqf  19447  filunirn  19582  fmf  19645  txflf  19706  clsnsg  19807  tgpconcomp  19810  divstgpopn  19817  divstgplem  19818  ustfn  19903  xmetunirn  20039  met1stc  20223  rrxmvallem  21030  ovolf  21092  vitali  21221  i1fmulc  21309  mbfi1fseqlem4  21324  itg2seq  21348  itg2monolem1  21356  i1fibl  21413  fncpn  21535  lhop1lem  21613  mdegxrf  21667  aannenlem3  21924  logccv  22236  padicabvf  23008  mptelee  23288  fngid  23848  grpoinvf  23874  occllem  24853  pjfni  25251  pjmfn  25265  rnbra  25658  bra11  25659  kbass2  25668  hmopidmchi  25702  xppreima2  26111  abfmpunirn  26113  dmct  26160  ofcfn  26682  sxbrsigalem3  26826  eulerpartgbij  26894  sseqfv1  26911  sseqfn  26912  sseqf  26914  sseqfv2  26916  fprodshft  27626  fprodrev  27627  faclimlem1  27688  mblfinlem2  28572  volsupnfl  28579  cnambfre  28583  itg2addnclem2  28587  itg2addnclem3  28588  ftc1anclem5  28614  ftc1anclem7  28616  sdclem2  28781  prdsbnd2  28837  rrncmslem  28874  rmxypairf1o  29395  hbtlem6  29628  dgraaf  29647  cytpfn  29719  addrfn  29871  subrfn  29872  mulvfn  29873  wlkiswwlk2lem1  30468  clwlkisclwwlklem2a2  30585  diafn  34998  cdlemm10N  35082  dibfna  35118  lcfrlem9  35514  mapd1o  35612  hdmapfnN  35796  hgmapfnN  35855