Theorem fdmi 6702

Description: Inference associated with fdm 6700. 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 6700	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐹 = 𝐴

Syntax hints:   = wceq 1540  dom cdm 5641  ⟶wf 6510

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 207  df-an 396  df-fn 6517  df-f 6518

This theorem is referenced by:  f0cli  7073  rankvaln  9759  isnum2  9905  r0weon  9972  cfub  10209  cardcf  10212  cflecard  10213  cfle  10214  cflim2  10223  cfidm  10235  cardf  10510  smobeth  10546  inar1  10735  addcompq  10910  addcomnq  10911  mulcompq  10912  mulcomnq  10913  adderpq  10916  mulerpq  10917  addassnq  10918  mulassnq  10919  distrnq  10921  recmulnq  10924  recclnq  10926  dmrecnq  10928  lterpq  10930  ltanq  10931  ltmnq  10932  ltexnq  10935  nsmallnq  10937  ltbtwnnq  10938  prlem934  10993  ltaddpr  10994  ltexprlem2  10997  ltexprlem3  10998  ltexprlem4  10999  ltexprlem6  11001  ltexprlem7  11002  prlem936  11007  eluzel2  12805  uzssz  12821  elixx3g  13326  ndmioo  13340  elfz2  13482  fz0  13507  elfzoel1  13625  elfzoel2  13626  fzoval  13628  ltweuz  13933  fzofi  13946  dmhashres  14313  s1dm  14580  s2dm  14863  sumz  15695  sumss  15697  prod1  15917  prodss  15920  znnen  16187  unbenlem  16886  prmreclem6  16899  eldmcoa  18034  efgsdm  19667  efgsval  19668  efgsp1  19674  efgsfo  19676  efgredleme  19680  efgred  19685  gexex  19790  torsubg  19791  dmdprd  19937  dprdval  19942  iocpnfordt  23109  icomnfordt  23110  uzrest  23791  qtopbaslem  24653  retopbas  24655  tgqioo  24695  re2ndc  24696  bndth  24864  tcphcph  25144  ovolficcss  25377  ismbl  25434  uniiccdif  25486  dyadmbllem  25507  opnmbllem  25509  opnmblALT  25511  mbfimaopnlem  25563  itg1addlem4  25607  dvcmul  25854  dvcmulf  25855  dvexp  25864  c1liplem1  25908  deg1n0ima  26001  pserulm  26338  psercn2  26339  psercn2OLD  26340  psercnlem2  26341  psercnlem1  26342  psercn  26343  pserdvlem1  26344  pserdvlem2  26345  pserdv  26346  pserdv2  26347  abelth  26358  efcn  26360  efcvx  26366  eff1olem  26464  dvrelog  26553  logf1o2  26566  dvlog  26567  efopn  26574  logtayl  26576  cxpcn3lem  26664  cxpcn3  26665  resqrtcn  26666  atancl  26798  atanval  26801  dvatan  26852  atancn  26853  bdaydm  27693  lltropt  27791  madess  27795  oldssmade  27796  madebdayim  27806  oldbdayim  27807  lrold  27815  madefi  27831  oldfi  27832  topnfbey  30405  cnaddabloOLD  30517  cnidOLD  30518  cncvcOLD  30519  cnnv  30613  cnnvba  30615  cncph  30755  dfhnorm2  31058  hilablo  31096  hilid  31097  hilvc  31098  hhnv  31101  hhba  31103  hhph  31114  issh2  31145  hhssabloi  31198  hhssnv  31200  hhshsslem1  31203  imaelshi  31994  rnelshi  31995  nlelshi  31996  xrofsup  32697  ply1degltel  33567  ply1degleel  33568  ply1degltlss  33569  coinfliprv  34481  erdszelem2  35186  erdszelem5  35189  erdszelem8  35192  msrrcl  35537  mthmsta  35572  icoreunrn  37354  icoreelrn  37356  relowlpssretop  37359  poimirlem26  37647  poimirlem27  37648  opnmbllem0  37657  dvtan  37671  fpwfvss  43408  seff  44305  sblpnf  44306  dvsconst  44326  dvsid  44327  dvsef  44328  expgrowth  44331  binomcxplemdvbinom  44349  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  addcomgi  44452  dmuz  45235  dmico  45568  dvsinax  45918  fvvolioof  45994  fvvolicof  45996  dirkercncflem2  46109  fourierdlem42  46154  hoicvr  46553  ovolval3  46652  fucofvalne  49318