Theorem fdmi 6498

Description: Inference associated with fdm 6495. The domain of a mapping. (Contributed by NM, 28-Jul-2008.)

Hypothesis

Ref	Expression
fdmi.1	⊢ 𝐹:𝐴⟶𝐵

Assertion

Ref	Expression
fdmi	⊢ dom 𝐹 = 𝐴

Proof of Theorem fdmi

Step	Hyp	Ref	Expression
1		fdmi.1	. 2 ⊢ 𝐹:𝐴⟶𝐵
2		fdm 6495	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐹 = 𝐴

Syntax hints:   = wceq 1538  dom cdm 5519  ⟶wf 6320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400  df-fn 6327  df-f 6328

This theorem is referenced by:  f0cli  6841  rankvaln  9212  isnum2  9358  r0weon  9423  cfub  9660  cardcf  9663  cflecard  9664  cfle  9665  cflim2  9674  cfidm  9686  cardf  9961  smobeth  9997  inar1  10186  addcompq  10361  addcomnq  10362  mulcompq  10363  mulcomnq  10364  adderpq  10367  mulerpq  10368  addassnq  10369  mulassnq  10370  distrnq  10372  recmulnq  10375  recclnq  10377  dmrecnq  10379  lterpq  10381  ltanq  10382  ltmnq  10383  ltexnq  10386  nsmallnq  10388  ltbtwnnq  10389  prlem934  10444  ltaddpr  10445  ltexprlem2  10448  ltexprlem3  10449  ltexprlem4  10450  ltexprlem6  10452  ltexprlem7  10453  prlem936  10458  eluzel2  12236  uzssz  12252  elixx3g  12739  ndmioo  12753  elfz2  12892  fz0  12917  elfzoel1  13031  elfzoel2  13032  fzoval  13034  ltweuz  13324  fzofi  13337  dmhashres  13697  s1dm  13953  s2dm  14243  sumz  15071  sumss  15073  prod1  15290  prodss  15293  znnen  15557  unbenlem  16234  prmreclem6  16247  eldmcoa  17317  efgsdm  18848  efgsval  18849  efgsp1  18855  efgsfo  18857  efgredleme  18861  efgred  18866  gexex  18966  torsubg  18967  dmdprd  19113  dprdval  19118  iocpnfordt  21820  icomnfordt  21821  uzrest  22502  qtopbaslem  23364  retopbas  23366  tgqioo  23405  re2ndc  23406  bndth  23563  tcphcph  23841  ovolficcss  24073  ismbl  24130  uniiccdif  24182  dyadmbllem  24203  opnmbllem  24205  opnmblALT  24207  mbfimaopnlem  24259  itg1addlem4  24303  dvcmul  24547  dvcmulf  24548  dvexp  24556  c1liplem1  24599  deg1n0ima  24690  pserulm  25017  psercn2  25018  psercnlem2  25019  psercnlem1  25020  psercn  25021  pserdvlem1  25022  pserdvlem2  25023  pserdv  25024  pserdv2  25025  abelth  25036  efcn  25038  efcvx  25044  eff1olem  25140  dvrelog  25228  logf1o2  25241  dvlog  25242  efopn  25249  logtayl  25251  cxpcn3lem  25336  cxpcn3  25337  resqrtcn  25338  atancl  25467  atanval  25470  dvatan  25521  atancn  25522  topnfbey  28254  cnaddabloOLD  28364  cnidOLD  28365  cncvcOLD  28366  cnnv  28460  cnnvba  28462  cncph  28602  dfhnorm2  28905  hilablo  28943  hilid  28944  hilvc  28945  hhnv  28948  hhba  28950  hhph  28961  issh2  28992  hhssabloi  29045  hhssnv  29047  hhshsslem1  29050  imaelshi  29841  rnelshi  29842  nlelshi  29843  xrofsup  30518  coinfliprv  31850  erdszelem2  32552  erdszelem5  32555  erdszelem8  32558  msrrcl  32903  mthmsta  32938  bdaydm  33357  icoreunrn  34776  icoreelrn  34778  relowlpssretop  34781  poimirlem26  35083  poimirlem27  35084  opnmbllem0  35093  dvtan  35107  seff  41013  sblpnf  41014  dvsconst  41034  dvsid  41035  dvsef  41036  expgrowth  41039  binomcxplemdvbinom  41057  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  addcomgi  41160  dmuz  41870  dmico  42202  dvsinax  42555  fvvolioof  42631  fvvolicof  42633  dirkercncflem2  42746  fourierdlem42  42791  hoicvr  43187  ovolval3  43286