Theorem fdm 5688

Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fdm	|- ( F : A --> B -> dom F = A )

Proof of Theorem fdm

Step	Hyp	Ref	Expression
1		ffn 5684	. 2 |- ( F : A --> B -> F Fn A )
2		fndm 5631	. 2 |- ( F Fn A -> dom F = A )
3	1, 2	syl 17	1 |- ( F : A --> B -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1437   dom cdm 4791   Fn wfn 5534   -->wf 5535

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 188  df-an 372  df-fn 5542  df-f 5543

This theorem is referenced by:  fdmi  5689  fssxp  5696  ffdm  5698  f00  5720  f0dom0  5722  f0rn0  5723  foima  5753  foco  5758  resdif  5789  fimacnv  5966  dff3  5989  ffvresb  6008  fmptco  6010  dmfex  6704  fornex  6715  frnsuppeq  6876  suppss  6895  onnseq  7013  issmo2  7018  smoiso  7031  mapprc  7426  elpm2r  7439  map0b  7460  mapsn  7463  brdomg  7529  pw2f1olem  7624  fopwdom  7628  fodomfib  7799  fisuppfi  7839  intrnfi  7878  ordtypelem5  7985  ordtypelem6  7986  ordtypelem7  7987  ordtypelem8  7988  wemapso2lem  8015  brwdomn0  8032  wdomtr  8038  cantnfcl  8119  cantnfle  8123  cantnflt  8124  cantnff  8126  cantnfp1lem3  8132  cantnflem1b  8138  cantnflem1d  8140  cantnflem1  8141  cantnflem3  8143  cnfcomlem  8151  cnfcom  8152  cnfcom2lem  8153  cnfcom3lem  8155  cnfcom3  8156  iunmapdisj  8400  fseqenlem2  8402  fodomfi2  8437  infmap2  8594  coftr  8649  fin23lem30  8718  fin23lem40  8727  isf34lem5  8754  isf34lem7  8755  isf34lem6  8756  fin1a2lem7  8782  axdc3lem2  8827  axdc3lem4  8829  ttukeylem6  8890  fodomb  8900  pwxpndom2  9036  rpnnen1lem4  11239  rpnnen1lem5  11240  fseqsupcl  12135  fseqsupubi  12136  hashimarn  12553  hashfzdm  12555  hashfirdm  12557  hashf1lem1  12561  wrddm  12621  swrdcl  12716  swrdnd2  12730  cats1un  12773  repswswrd  12828  limsupgle  13473  limsupgre  13480  limsupgreOLD  13481  rlim  13497  rlimi  13515  ello12  13518  lo1bdd  13522  elo12  13529  o1bdd  13533  lo1o1  13534  rlimclim  13548  rlimuni  13552  o1co  13588  rlimcn1  13590  isercolllem2  13667  isercolllem3  13668  fsumss  13729  fprodss  13940  ruclem11  14230  1arith  14809  vdwlem1  14869  vdwlem5  14873  vdwlem6  14874  vdwlem11  14879  ramval  14898  ramvalOLD  14899  0ram  14916  0ram2  14917  0ramcl  14919  mrcuni  15465  homarcl2  15868  prfval  16022  intopsn  16436  gsumval  16452  gsumval2  16461  ghmrn  16834  ghmpreima  16842  cntzmhm2  16931  symgfixf1  17016  f1omvdconj  17025  pmtrfconj  17045  pmtrdifellem1  17055  pmtrdifellem2  17056  gsumval3lem1  17477  gsumval3lem2  17478  gsumval3  17479  gsumzres  17481  gsumzcl2  17482  gsumzf1o  17484  gsumzaddlem  17492  gsumzmhm  17508  gsumzoppg  17515  gsum2d  17542  dmdprdd  17569  dprdres  17599  dprdss  17600  dprdf1  17604  dmdprdsplitlem  17608  dprd2da  17613  dmdprdsplit2lem  17616  dmdprdsplit2  17617  dmdprdsplit  17618  dprdsplit  17619  dpjidcl  17629  ablfac1eulem  17643  ablfac1eu  17644  ablfaclem2  17657  ablfaclem3  17658  ablfac2  17660  lmhmpreima  18209  lmhmlsp  18210  mplcoe1  18627  mplcoe5  18630  psr1baslem  18716  gsumfsum  18972  evpmss  19091  regsumsupp  19127  pjdm2  19211  frlmlbs  19292  islindf2  19309  f1lindf  19317  islindf4  19333  mattpostpos  19416  mdetdiaglem  19560  decpmatval  19726  pmatcollpw3lem  19744  iinopn  19869  iscnp3  20197  lmbrf  20213  cnpnei  20217  cnclima  20221  iscncl  20222  cnntri  20224  cnclsi  20225  cncls2  20226  cncls  20227  cnntr  20228  cncnp  20233  cndis  20244  paste  20247  lmcnp  20257  cnt0  20299  cnt1  20303  cnhaus  20307  cncmp  20344  imacmp  20349  hauscmplem  20358  cnconn  20374  conima  20377  1stcfb  20397  1stccnp  20414  1stckgenlem  20505  kgencn  20508  kgencn3  20510  txcnpi  20560  txcnp  20572  txcnmpt  20576  prdstps  20581  xkohaus  20605  xkopt  20607  xkoco2cn  20610  xkococnlem  20611  qtopval2  20648  qtopcn  20666  qtopeu  20668  hmeores  20723  fbasrn  20836  fmval  20895  fmf  20897  rnelfmlem  20904  rnelfm  20905  fmfnfmlem2  20907  fmfnfmlem4  20909  fmfnfm  20910  cnflf2  20955  lmflf  20957  txflf  20958  cnextfval  21014  cnextcn  21019  clssubg  21060  ghmcnp  21066  tgphaus  21068  qustgplem  21072  tsmsval  21082  tsmsgsum  21090  ucncn  21237  psmetdmdm  21258  xmetdmdm  21287  metn0  21312  xmetres  21316  metres  21317  xmeter  21385  tmsval  21433  metcnp  21493  metustss  21503  metustid  21506  metustsym  21507  metustexhalf  21508  metustfbas  21509  cfilucfil  21511  metuel2  21517  restmetu  21522  isngp2  21548  evth  21924  lmmbrf  22169  iscfil2  22173  caufval  22182  iscau2  22184  iscauf  22187  caucfil  22190  equivcau  22207  lmclimf  22210  rrxcph  22288  rrxsuppss  22294  ovollb2  22379  ovolunlem1a  22386  ovoliunlem1  22392  ovoliun2  22396  ioombl1lem4  22451  uniioombllem1  22475  uniioombllem2  22477  uniioombllem2OLD  22478  uniioombllem6  22483  mbfconstlem  22522  ismbf  22523  ismbfcn  22524  mbfimaicc  22526  mbfmulc2lem  22540  mbfmulc2re  22541  mbfimaopn2  22550  cncombf  22551  mbfaddlem  22553  mbflimsup  22560  mbflimsupOLD  22561  i1f0rn  22577  itg1addlem5  22595  itg1climres  22609  mbfmullem2  22619  ibl0  22681  cniccibl  22735  limcfval  22764  limcdif  22768  ellimc2  22769  ellimc3  22771  limccnp  22783  dvfval  22789  cpnord  22826  cpnres  22828  dvcmul  22835  dvcmulf  22836  dvnfre  22843  dvexp  22844  c1liplem1  22885  c1lip2  22887  dvgt0lem1  22891  dvcnvrelem1  22906  dvcnvrelem2  22907  mdegfval  22948  mdegleb  22950  mdegldg  22952  deg1mul3le  23002  plyco0  23083  plyeq0lem  23101  plyeq0  23102  plyaddlem1  23104  plymullem1  23105  dgrcl  23124  dgrub  23125  dgrlb  23127  plycpn  23179  vieta1lem1  23200  vieta1lem2  23201  aalioulem3  23227  taylfvallem1  23249  tayl0  23254  taylply2  23260  taylply  23261  dvtaylp  23262  dvntaylp  23263  dvntaylp0  23264  taylthlem1  23265  taylthlem2  23266  ulm2  23277  ulmss  23289  ulmdvlem1  23292  ulmdvlem2  23293  ulmdvlem3  23294  itgulm  23300  xrlimcnp  23831  basellem5  23948  dchrelbas2  24102  dchrghm  24121  dchrptlem1  24129  dchrptlem2  24130  iscgrgd  24495  iscgrglt  24496  trgcgrg  24497  tgcgr4  24513  motcgrg  24526  eedimeq  24865  axcontlem10  24940  uhgraun  24975  wrdumgra  24980  umgra1  24990  umgraun  24992  wlkn0  25192  eupares  25640  grporndm  25875  resgrprn  25945  isabloda  25964  subgores  25969  ismgmOLD  25985  ismndo2  26010  ghsubgolemOLD  26035  rngodm1dm2  26083  rngosn3  26091  vcoprne  26135  nvdm  26227  sspn  26312  dmadjrnb  27496  elnlfn  27518  xppreima  28189  fmptcof2  28200  curry2ima  28230  fpwrelmap  28263  smatrcl  28569  mdetpmtr1  28596  locfinreflem  28614  hauseqcn  28648  rge0scvg  28702  indpreima  28793  indf1ofs  28794  esumpcvgval  28846  ofcfval4  28873  isrnmeas  28969  measdivcst  28994  omsfval  29065  omscl  29066  omsf  29067  omsfvalOLD  29069  omsclOLD  29070  omsfOLD  29071  oms0  29072  omsmon  29073  omssubaddlem  29074  omssubadd  29075  oms0OLD  29076  omsmonOLD  29077  omssubaddlemOLD  29078  omssubaddOLD  29079  carsgval  29082  carsggect  29097  omsmeas  29102  omsmeasOLD  29103  sibfof  29120  sitgclg  29122  eulerpartlemsv2  29138  eulerpartlemsf  29139  eulerpartlemv  29144  eulerpartlemd  29146  eulerpartlemb  29148  eulerpartlemt  29151  eulerpartlemr  29154  eulerpartlemgvv  29156  eulerpartlemgu  29157  eulerpartlemgs2  29160  eulerpartlemn  29161  sseqfv2  29174  rrvdm  29226  cvmliftmolem1  29951  cvmliftlem3  29957  cvmliftlem10  29964  cvmliftlem13  29966  cvmlift2lem9  29981  cvmlift3lem6  29994  cvmlift3lem7  29995  mrsubfval  30093  mclsax  30154  mclsppslem  30168  mclspps  30169  ghomfo  30256  soseq  30438  nodmon  30483  fwddifval  30873  fwddifnval  30874  ivthALT  30935  bj-finsumval0  31609  ptrecube  31847  heicant  31882  mbfresfi  31894  itg2addnclem  31900  itg2addnclem2  31901  cnicciblnc  31920  ftc1anclem1  31924  ftc1anclem5  31928  ftc1anclem6  31929  ftc1anclem8  31931  indexdom  31968  sdclem2  31978  cnres2  32002  sstotbnd2  32013  isbnd3  32023  ssbnd  32027  bnd2lem  32030  ismtyval  32039  exidreslem  32082  grpokerinj  32090  divrngcl  32103  isdrngo2  32104  keridl  32172  ismrcd1  35452  istopclsd  35454  mapfzcons2  35473  coeq0i  35507  pw2f1ocnv  35805  fnwe2lem2  35822  lmhmfgima  35855  pwfi2f1o  35867  cnioobibld  36011  itgpowd  36012  wnefimgd  36513  funfvima2d  36525  binomcxplemnotnn0  36618  cncmpmax  37269  fresin2  37339  evthiccabs  37485  mullimcf  37586  cncfuni  37647  cncficcgt0  37649  cncfioobd  37658  dvsinax  37666  dvsubcncf  37679  dvmulcncf  37680  dvdivcncf  37682  cnbdibl  37722  itgperiod  37741  stoweidlem29  37772  stoweidlem29OLD  37773  fourierdlem20  37872  fourierdlem48  37901  fourierdlem49  37902  fourierdlem53  37906  fourierdlem58  37911  fourierdlem59  37912  fourierdlem63  37916  fourierdlem68  37921  fourierdlem71  37924  fourierdlem73  37926  fourierdlem74  37927  fourierdlem75  37928  fourierdlem76  37929  fourierdlem80  37933  fourierdlem81  37934  fourierdlem82  37935  fourierdlem89  37942  fourierdlem91  37944  fourierdlem92  37945  fourierdlem93  37946  fourierdlem94  37947  fourierdlem111  37964  fourierdlem112  37965  fourierdlem113  37966  fouriercn  37979  sge0val  38059  fge0iccico  38063  sge0sn  38072  sge0tsms  38073  sge0cl  38074  sge0f1o  38075  sge0isum  38120  ismeannd  38156  isomennd  38203  hoicvr  38217  nnsum4primeseven  38708  nnsum4primesevenALTV  38709  uhgrun  38942  wrdupgr  38951  wrdumgr  38961  upgr1e  38971  upgrun  38976  umgrun  38978  uhgun  39283  domnmsuppn0  39747  rmsuppss  39748  mndpsuppss  39749  scmsuppss  39750  fdivmpt  39944  fdivmptf  39945  refdivmptf  39946  fdivpm  39947  refdivpm  39948  elbigo2  39956  elbigolo1  39961