MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fdmi Structured version   Visualization version   GIF version

Theorem fdmi 6505
Description: Inference associated with fdm 6502. 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
StepHypRef Expression
1 fdmi.1 . 2 𝐹:𝐴𝐵
2 fdm 6502 . 2 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
31, 2ax-mp 5 1 dom 𝐹 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  dom cdm 5532  wf 6330
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 6337  df-f 6338
This theorem is referenced by:  f0cli  6846  rankvaln  9216  isnum2  9362  r0weon  9427  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  15070  sumss  15072  prod1  15289  prodss  15292  znnen  15556  unbenlem  16233  prmreclem6  16246  eldmcoa  17316  efgsdm  18847  efgsval  18848  efgsp1  18854  efgsfo  18856  efgredleme  18860  efgred  18865  gexex  18964  torsubg  18965  dmdprd  19111  dprdval  19116  iocpnfordt  21818  icomnfordt  21819  uzrest  22500  qtopbaslem  23362  retopbas  23364  tgqioo  23403  re2ndc  23404  bndth  23561  tcphcph  23839  ovolficcss  24071  ismbl  24128  uniiccdif  24180  dyadmbllem  24201  opnmbllem  24203  opnmblALT  24205  mbfimaopnlem  24257  itg1addlem4  24301  dvcmul  24545  dvcmulf  24546  dvexp  24554  c1liplem1  24597  deg1n0ima  24688  pserulm  25015  psercn2  25016  psercnlem2  25017  psercnlem1  25018  psercn  25019  pserdvlem1  25020  pserdvlem2  25021  pserdv  25022  pserdv2  25023  abelth  25034  efcn  25036  efcvx  25042  eff1olem  25138  dvrelog  25226  logf1o2  25239  dvlog  25240  efopn  25247  logtayl  25249  cxpcn3lem  25334  cxpcn3  25335  resqrtcn  25336  atancl  25465  atanval  25468  dvatan  25519  atancn  25520  topnfbey  28252  cnaddabloOLD  28362  cnidOLD  28363  cncvcOLD  28364  cnnv  28458  cnnvba  28460  cncph  28600  dfhnorm2  28903  hilablo  28941  hilid  28942  hilvc  28943  hhnv  28946  hhba  28948  hhph  28959  issh2  28990  hhssabloi  29043  hhssnv  29045  hhshsslem1  29048  imaelshi  29839  rnelshi  29840  nlelshi  29841  xrofsup  30502  coinfliprv  31814  erdszelem2  32513  erdszelem5  32516  erdszelem8  32519  msrrcl  32864  mthmsta  32899  bdaydm  33318  icoreunrn  34737  icoreelrn  34739  relowlpssretop  34742  poimirlem26  35041  poimirlem27  35042  opnmbllem0  35051  dvtan  35065  seff  40947  sblpnf  40948  dvsconst  40968  dvsid  40969  dvsef  40970  expgrowth  40973  binomcxplemdvbinom  40991  binomcxplemdvsum  40993  binomcxplemnotnn0  40994  addcomgi  41094  dmuz  41808  dmico  42141  dvsinax  42494  fvvolioof  42570  fvvolicof  42572  dirkercncflem2  42685  fourierdlem42  42730  hoicvr  43126  ovolval3  43225
  Copyright terms: Public domain W3C validator