Theorem dmmpti 6683

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 6682	. 2 ⊢ 𝐹 Fn 𝐴
4	3	fndmi 6643	1 ⊢ dom 𝐹 = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  Vcvv 3457   ↦ cmpt 5194  dom cdm 5663

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:  fvmptex  7008  resfunexg  7220  brtpos2  8234  pwfilem  9284  inlresf  9916  inrresf  9918  sgndm  15159  vdwlem8  17072  oppccatf  17808  lubdm  18429  glbdm  18442  mndpsuppss  18862  dprd2dlem2  20158  dprd2dlem1  20159  dprd2da  20160  ablfac1c  20189  ablfac1eu  20191  ablfaclem2  20204  ablfaclem3  20205  elocv  21870  dmtopon  23132  dfac14  23828  kqtop  23955  symgtgp  24316  eltsms  24343  ressprdsds  24581  minveclem1  25636  isi1f  25886  itg1val  25895  cmvth  26203  mvth  26204  lhop2  26227  dvfsumabs  26235  dvfsumrlim2  26244  taylthlem1  26589  taylthlem2  26590  ulmdvlem1  26616  pige3ALT  26738  relogcn  26856  atandm  27094  atanf  27098  atancn  27154  dmarea  27175  dfarea  27178  efrlim  27187  lgamgulmlem2  27247  dchrptlem2  27482  dchrptlem3  27483  dchrisum0  27737  nosupno  27920  nosupdm  27921  nosupbday  27922  nosupres  27924  nosupbnd1lem1  27925  noinfno  27935  noinfdm  27936  incistruhgr  29486  vsfval  31058  ipasslem8  31262  minvecolem1  31299  xppreima2  33069  ofpreima  33083  rmfsupp2  33623  zarclsint  34328  zartopn  34331  zarmxt1  34336  zarcmplem  34337  dmsigagen  34601  measbase  34654  sseqf  34849  ballotlem7  34993  bj-inftyexpitaudisj  37908  bj-inftyexpidisj  37913  bj-elccinfty  37917  bj-minftyccb  37928  fin2so  38317  poimirlem30  38360  poimir  38363  dvtan  38380  itg2addnclem2  38382  ftc1anclem6  38408  totbndbnd  38500  tfsconcatrev  44135  comptiunov2i  44492  lhe4.4ex1a  45099  dvsinax  46687  fourierdlem62  46942  fourierdlem70  46950  fourierdlem71  46951  fourierdlem80  46960  fouriersw  47005  smflimsuplem1  47594  smflimsuplem4  47597  scmsuppss  49210  lincext2  49294  idfurcl  49935  reldmprcof1  50218  reldmlmd2  50490  reldmcmd2  50491  aacllem  50680