Theorem dmmpti 6688

Description: Domain of the mapping operation. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 31-Aug-2015.)

Hypotheses

Ref	Expression
fnmpti.1	⊢ 𝐵 ∈ V
fnmpti.2	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
dmmpti	⊢ dom 𝐹 = 𝐴

Distinct variable group:   𝑥,𝐴

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

Proof of Theorem dmmpti

Step	Hyp	Ref	Expression
1		fnmpti.1	. . 3 ⊢ 𝐵 ∈ V
2		fnmpti.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	1, 2	fnmpti 6687	. 2 ⊢ 𝐹 Fn 𝐴
4	3	fndmi 6648	1 ⊢ dom 𝐹 = 𝐴

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  Vcvv 3450   ↦ cmpt 5185  dom cdm 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-fun 6545  df-fn 6546

This theorem is used by:  fvmptex  7013  resfunexg  7225  brtpos2  8257  pwfilem  9317  inlresf  10002  inrresf  10004  sgndm  15258  vdwlem8  17175  oppccatf  17911  lubdm  18532  glbdm  18545  mndpsuppss  18968  dprd2dlem2  20265  dprd2dlem1  20266  dprd2da  20267  ablfac1c  20296  ablfac1eu  20298  ablfaclem2  20311  ablfaclem3  20312  elocv  21983  dmtopon  23250  dfac14  23946  kqtop  24073  symgtgp  24434  eltsms  24461  ressprdsds  24699  minveclem1  25754  isi1f  26004  itg1val  26013  cmvth  26320  mvth  26321  lhop2  26344  dvfsumabs  26352  dvfsumrlim2  26361  taylthlem1  26709  taylthlem2  26710  ulmdvlem1  26736  pige3ALT  26857  relogcn  26975  atandm  27213  atanf  27217  atancn  27273  dmarea  27294  dfarea  27297  efrlim  27306  lgamgulmlem2  27366  dchrptlem2  27601  dchrptlem3  27602  dchrisum0  27856  nosupno  28069  nosupdm  28070  nosupbday  28071  nosupres  28073  nosupbnd1lem1  28074  noinfno  28084  noinfdm  28085  incistruhgr  29666  vsfval  31244  ipasslem8  31448  minvecolem1  31485  xppreima2  33296  ofpreima  33310  rmfsupp2  33848  zarclsint  34554  zartopn  34557  zarmxt1  34562  zarcmplem  34563  dmsigagen  34827  measbase  34880  sseqf  35074  ballotlem7  35218  bj-inftyexpitaudisj  38263  bj-inftyexpidisj  38268  bj-elccinfty  38272  bj-minftyccb  38283  fin2so  38667  poimirlem30  38705  poimir  38708  dvtan  38725  itg2addnclem2  38727  ftc1anclem6  38753  totbndbnd  38860  tfsconcatrev  44487  comptiunov2i  44843  lhe4.4ex1a  45450  dvsinax  47059  fourierdlem62  47314  fourierdlem70  47322  fourierdlem71  47323  fourierdlem80  47332  fouriersw  47377  smflimsuplem1  47966  smflimsuplem4  47969  scmsuppss  49619  lincext2  49703  idfurcl  50350  reldmprcof1  50652  reldmlmd2  50972  reldmcmd2  50973  aacllem  51150