Theorem fnmpti 6474

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 3065	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
3		fnmpti.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	mptfng 6470	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
5	2, 4	mpbi 233	1 ⊢ 𝐹 Fn 𝐴

Syntax hints:   = wceq 1542   ∈ wcel 2113  ∀wral 3053  Vcvv 3397   ↦ cmpt 5107   Fn wfn 6328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ral 3058  df-v 3399  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-sn 4514  df-pr 4516  df-op 4520  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-fun 6335  df-fn 6336

This theorem is referenced by:  dmmpti  6475  fconst  6558  dffn5  6722  idref  6912  eufnfv  6996  offn  7431  caofinvl  7448  fo1st  7727  fo2nd  7728  reldm  7761  fimaproj  7848  mapsnf1o2  8497  unfilem2  8850  fidomdm  8867  pwfilemOLD  8884  noinfep  9189  aceq3lem  9613  dfac4  9615  ackbij2lem2  9733  cfslb2n  9761  axcc2lem  9929  dmct  10017  konigthlem  10061  rankcf  10270  tskuni  10276  seqf1o  13496  ccatlen  14009  ccatlenOLD  14010  ccatvalfn  14017  swrdlen  14091  swrdwrdsymb  14106  swrdswrd  14149  sqrtf  14806  mptfzshft  15219  efcvgfsum  15524  prmreclem2  16346  1arith  16356  vdwlem6  16415  vdwlem8  16417  slotfn  16597  topnfn  16795  fnmre  16958  cidffn  17045  cidfn  17046  funcres  17264  initofn  17352  termofn  17353  zeroofn  17354  yonedainv  17640  fn0g  17982  smndex1igid  18178  smndex1n0mnd  18186  grpinvfn  18256  cycsubmel  18454  conjnmz  18503  psgnfn  18740  odf  18776  sylow1lem4  18837  pgpssslw  18850  sylow2blem3  18858  sylow3lem2  18864  cygctb  19124  dprd2da  19276  fnmgp  19353  rlmfn  20074  rrgsupp  20176  frlmup4  20610  asclfn  20687  evlslem1  20889  mdetrlin  21346  fncld  21766  hauseqlcld  22390  kqf  22491  filunirn  22626  fmf  22689  txflf  22750  clsnsg  22854  tgpconncomp  22857  qustgpopn  22864  qustgplem  22865  ustfn  22946  xmetunirn  23083  met1stc  23267  rrxmvallem  24149  ovolf  24227  vitali  24358  i1fmulc  24448  mbfi1fseqlem4  24463  itg2seq  24487  itg2monolem1  24495  i1fibl  24552  fncpn  24677  lhop1lem  24757  mdegxrf  24813  aannenlem3  25070  efabl  25286  logccv  25398  gausslemma2dlem1  26094  padicabvf  26359  mptelee  26833  wlkiswwlks2lem1  27799  clwlkclwwlklem2a2  27922  grpoinvf  28459  occllem  29230  pjfni  29628  pjmfn  29642  rnbra  30034  bra11  30035  kbass2  30044  hmopidmchi  30078  xppreima2  30554  abfmpunirn  30556  psgnfzto1stlem  30936  elrspunidl  31170  locfinreflem  31354  zarclsint  31386  zar0ring  31392  rhmpreimacn  31399  ofcfn  31630  sxbrsigalem3  31801  eulerpartgbij  31901  sseqfv1  31918  sseqfn  31919  sseqf  31921  sseqfv2  31923  signstlen  32108  msubrn  33054  msrf  33067  faclimlem1  33272  bj-evalfn  34855  bj-inftyexpitaufo  34983  matunitlindflem1  35385  poimirlem30  35419  mblfinlem2  35427  volsupnfl  35434  cnambfre  35437  itg2addnclem2  35441  itg2addnclem3  35442  ftc1anclem5  35466  ftc1anclem7  35468  sdclem2  35512  prdsbnd2  35565  rrncmslem  35602  diafn  38660  cdlemm10N  38744  dibfna  38780  lcfrlem9  39176  mapd1o  39274  hdmapfnN  39455  hgmapfnN  39514  evlsbagval  39838  fsuppind  39842  mhphf  39848  rmxypairf1o  40289  hbtlem6  40510  dgraaf  40528  cytpfn  40589  ntrf  41263  uzmptshftfval  41486  binomcxplemrat  41490  addrfn  41612  subrfn  41613  mulvfn  41614  limsup10exlem  42839  liminfvalxr  42850  fourierdlem62  43235  fourierdlem70  43243  fourierdlem71  43244  fmtnorn  44504  zrinitorngc  45076  zrtermorngc  45077  zrtermoringc  45146