Theorem fdmi 6721

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

This proof depends on syntax axioms:   = wceq 1569  dom cdm 5650  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6541  df-f 6542

This theorem is used by:  f0cli  7098  rankvaln  9808  isnum2  10027  r0weon  10092  cfub  10327  cardcf  10330  cflecard  10331  cfle  10332  cflim2  10342  cfidm  10354  cardf  10635  smobeth  10672  inar1  10861  addcompq  11036  addcomnq  11037  mulcompq  11038  mulcomnq  11039  adderpq  11042  mulerpq  11043  addassnq  11044  mulassnq  11045  distrnq  11047  recmulnq  11050  recclnq  11052  dmrecnq  11054  lterpq  11056  ltanq  11057  ltmnq  11058  ltexnq  11061  nsmallnq  11063  ltbtwnnq  11064  prlem934  11119  ltaddpr  11120  ltexprlem2  11123  ltexprlem3  11124  ltexprlem4  11125  ltexprlem6  11127  ltexprlem7  11128  prlem936  11133  eluzel2  12971  uzssz  12987  elixx3g  13490  ndmioo  13504  elfz2  13647  fz0  13673  elfzoel1  13792  elfzoel2  13793  fzoval  13795  ltweuz  14105  fzofi  14118  dmhashres  14486  s1dm  14756  s2dm  15042  sumz  15889  sumss  15891  prod1  16112  prodss  16115  znnen  16381  unbenlem  17087  prmreclem6  17100  eldmcoa  18241  efgsdm  19945  efgsval  19946  efgsp1  19952  efgsfo  19954  efgredleme  19958  efgred  19963  gexex  20068  torsubg  20069  dmdprd  20215  dprdval  20220  iocpnfordt  23534  icomnfordt  23535  uzrest  24217  qtopbaslem  25078  retopbas  25080  tgqioo  25120  re2ndc  25121  bndth  25280  tcphcph  25559  ovolficcss  25791  ismbl  25848  uniiccdif  25900  dyadmbllem  25921  opnmbllem  25923  opnmblALT  25925  mbfimaopnlem  25977  itg1addlem4  26021  dvcmul  26265  dvcmulf  26266  dvexp  26274  c1liplem1  26317  deg1n0ima  26408  pserulm  26750  psercn2  26751  psercnlem2  26752  psercnlem1  26753  psercn  26754  pserdvlem1  26755  pserdvlem2  26756  pserdv  26757  pserdv2  26758  abelth  26769  efcn  26771  efcvx  26777  eff1olem  26877  dvrelog  26966  logf1o2  26979  dvlog  26980  efopn  26987  logtayl  26989  cxpcn3lem  27076  cxpcn3  27077  resqrtcn  27078  atancl  27210  atanval  27213  dvatan  27264  atancn  27265  bdaydmOLD  28137  lltr  28249  madess  28253  oldssmade  28254  oldss  28257  madebdayim  28275  oldbdayim  28276  lrold  28284  madefi  28300  oldfi  28301  cutminmax  28323  oldfib  28764  topnfbey  31071  cnaddabloOLD  31184  cnidOLD  31185  cncvcOLD  31186  cnnv  31280  cnnvba  31282  cncph  31422  dfhnorm2  31725  hilablo  31763  hilid  31764  hilvc  31765  hhnv  31768  hhba  31770  hhph  31781  issh2  31812  hhssabloi  31865  hhssnv  31867  hhshsslem1  31870  imaelshi  32661  rnelshi  32662  nlelshi  32663  xrofsup  33402  ply1degltel  34169  ply1degleel  34170  ply1degltlss  34171  coinfliprv  35158  dfscott3  35790  j00smo  35937  erdszelem2  36026  erdszelem5  36029  erdszelem8  36032  msrrcl  36377  mthmsta  36412  icoreunrn  38358  icoreelrn  38360  relowlpssretop  38363  poimirlem26  38640  poimirlem27  38641  opnmbllem0  38650  dvtan  38664  fpwfvss  44489  seff  45369  sblpnf  45370  dvsconst  45390  dvsid  45391  dvsef  45392  expgrowth  45395  binomcxplemdvbinom  45413  binomcxplemdvsum  45415  binomcxplemnotnn0  45416  addcomgi  45514  dmuz  46322  dmico  46651  dvsinax  46999  fvvolioof  47075  fvvolicof  47077  dirkercncflem2  47190  fourierdlem42  47235  hoicvr  47634  ovolval3  47733  tannpoly  48016  sinnpoly  48017  fucofvalne  50509  dvsec  50932  dvcsc  50933  dvcot  50934