Theorem fnmpti 6682

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	⊢ 𝐵 ∈ V
fnmpti.2	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
fnmpti	⊢ 𝐹 Fn 𝐴

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem fnmpti

Step	Hyp	Ref	Expression
1		fnmpti.1	. . 3 ⊢ 𝐵 ∈ V
2	1	rgenw 3085	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
3		fnmpti.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	mptfng 6678	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
5	2, 4	mpbi 233	1 ⊢ 𝐹 Fn 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  ∀wral 3081  Vcvv 3457   ↦ cmpt 5194   Fn wfn 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-fun 6542  df-fn 6543

This theorem is used by:  dmmpti  6683  fconst  6768  dffn5  6943  idref  7148  eufnfv  7234  offn  7697  caofinvl  7716  fo1st  8012  fo2nd  8013  reldm  8047  fimaproj  8137  mapsnf1o2  8898  unfilem2  9273  fidomdm  9298  noinfep  9636  ssttrcl  9691  ttrcltr  9692  ttrclselem2  9702  aceq3lem  10120  dfac4  10122  ackbij2lem2  10238  cfslb2n  10267  axcc2lem  10435  dmct  10523  konigthlem  10570  rankcf  10779  tskuni  10785  seqf1o  14099  ccatlen  14632  ccatvalfn  14638  swrdlen  14707  swrdwrdsymb  14724  swrdswrd  14766  sqrtf  15441  mptfzshft  15854  efcvgfsum  16164  prmreclem2  17001  1arith  17011  vdwlem6  17070  vdwlem8  17072  slotfn  17268  topnfn  17502  fnmre  17667  cidffn  17758  cidfn  17759  funcres  17977  initofn  18068  termofn  18069  zeroofn  18070  yonedainv  18361  fn0g  18748  smndex1igid  19004  smndex1igidOLD  19005  smndex1n0mnd  19013  grpinvfn  19094  cycsubmel  19317  conjnmz  19368  ghmquskerco  19400  psgnfn  19617  odf  19653  sylow1lem4  19717  pgpssslw  19730  sylow2blem3  19738  sylow3lem2  19744  cygctb  20008  dprd2da  20160  fnmgp  20264  zrinitorngc  20793  zrtermorngc  20794  zrtermoringc  20826  rrgsupp  20852  rlmfn  21363  frlmup4  22003  asclfn  22082  evlslem1  22285  evlsvvval  22296  psdmplcl  22377  psdadd  22378  psdmul  22381  psdmvr  22384  mdetrlin  22811  fncld  23231  hauseqlcld  23856  kqf  23957  filunirn  24092  fmf  24155  txflf  24216  clsnsg  24320  tgpconncomp  24323  qustgpopn  24330  qustgplem  24331  ustfn  24412  xmetunirn  24547  met1stc  24731  rrxmvallem  25616  ovolf  25694  vitali  25825  i1fmulc  25915  mbfi1fseqlem4  25930  itg2seq  25954  itg2monolem1  25962  i1fibl  26020  fncpn  26145  lhop1lem  26225  mdegxrf  26278  aannenlem3  26546  efabl  26768  logccv  26881  gausslemma2dlem1  27583  padicabvf  27848  mpteleeOLD  29302  wlkiswwlks2lem1  30287  clwlkclwwlklem2a2  30413  grpoinvf  30957  occllem  31728  pjfni  32126  pjmfn  32140  rnbra  32532  bra11  32533  kbass2  32542  hmopidmchi  32576  xppreima2  33069  abfmpunirn  33070  psgnfzto1stlem  33486  elrspunidl  33802  locfinreflem  34296  zarclsint  34328  zar0ring  34334  rhmpreimacn  34341  ofcfn  34556  sxbrsigalem3  34729  eulerpartgbij  34829  sseqfv1  34846  sseqfn  34847  sseqf  34849  sseqfv2  34851  signstlen  35021  kardfn  35623  vonf1oonfo  35658  msubrn  36060  msrf  36073  faclimlem1  36274  weiunlem  37033  bj-evalfn  37774  bj-inftyexpitaufo  37905  matunitlindflem1  38326  poimirlem30  38360  mblfinlem2  38368  volsupnfl  38375  cnambfre  38378  itg2addnclem2  38382  itg2addnclem3  38383  ftc1anclem5  38407  ftc1anclem7  38409  sdclem2  38453  prdsbnd2  38506  rrncmslem  38543  diafn  41868  cdlemm10N  41952  dibfna  41988  lcfrlem9  42384  mapd1o  42482  hdmapfnN  42663  hgmapfnN  42722  fsuppind  43382  rmxypairf1o  43698  hbtlem6  43916  dgraaf  43934  cytpfn  43988  tfsconcatrev  44135  ntrf  44909  uzmptshftfval  45116  binomcxplemrat  45120  addrfn  45240  subrfn  45241  mulvfn  45242  limsup10exlem  46546  liminfvalxr  46557  fourierdlem62  46942  fourierdlem70  46950  fourierdlem71  46951  cjnpoly  47686  fmtnorn  48346  tposideq  49725  cicfn  49879  fucofn22  50177  fucoid  50185  dfinito4  50338  crosspaltd  50707  crossp3d  50708