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

Theorem fmptd 6606
Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)
Hypotheses
Ref Expression
fmptd.1 ((𝜑𝑥𝐴) → 𝐵𝐶)
fmptd.2 𝐹 = (𝑥𝐴𝐵)
Assertion
Ref Expression
fmptd (𝜑𝐹:𝐴𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem fmptd
StepHypRef Expression
1 fmptd.1 . . 3 ((𝜑𝑥𝐴) → 𝐵𝐶)
21ralrimiva 3154 . 2 (𝜑 → ∀𝑥𝐴 𝐵𝐶)
3 fmptd.2 . . 3 𝐹 = (𝑥𝐴𝐵)
43fmpt 6602 . 2 (∀𝑥𝐴 𝐵𝐶𝐹:𝐴𝐶)
52, 4sylib 209 1 (𝜑𝐹:𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wcel 2156  wral 3096  cmpt 4923  wf 6097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-fv 6109
This theorem is referenced by:  fmpttd  6607  fnwelem  7526  fdiagfn  8138  resixpfo  8183  xpmapenlem  8366  unxpdomlem3  8405  fsuppmptdm  8525  cantnfp1lem1  8822  cantnfp1lem2  8823  cantnfp1lem3  8824  cantnf  8837  updjudhf  9040  fseqenlem2  9131  dfac8clem  9138  coftr  9380  isf34lem2  9480  axcc2lem  9543  axdc2lem  9555  axdc3lem4  9560  pwcfsdom  9690  rpnnen1lem1  12034  caucvg  14632  sumrblem  14665  summolem2a  14669  supcvg  14810  prodrblem  14880  prodmolem2a  14885  crth  15700  eulerthlem1  15703  prmreclem6  15842  4sqlem11  15876  vdwlem2  15903  vdwlem4  15905  vdwlem6  15907  vdwlem10  15911  ramub1lem2  15948  prmgaplcm  15981  frmdup1  17606  grpinvf  17671  cycsubgcl  17822  cycsubgss  17823  conjghm  17893  conjnmz  17896  qusghm  17899  galactghm  18024  symgextf  18038  symgfixf  18057  pmtrdifwrdellem1  18102  odf1  18180  dfod2  18182  pgpssslw  18230  frgpmhm  18379  gsummptfidmsplitres  18532  gsummptfidminv  18548  gsumzunsnd  18556  gsummpt1n0  18565  ablfac1b  18671  ablfac2  18690  abvtrivd  19044  issrngd  19065  pwssplit0  19265  asclf  19546  psr1cl  19611  evlslem1  19723  evlsval2  19728  mulgghm2  20053  isphld  20209  pjff  20266  frlmup1  20347  scmatf  20546  mdetf  20612  maduf  20658  pmatcollpw3fi1lem1  20804  chfacfisf  20872  chfacfisfcpmat  20873  cpmidpmatlem2  20889  lly1stc  21513  txcnmpt  21641  txlm  21665  xkoinjcn  21704  kqffn  21742  txflf  22023  tsmsfbas  22144  ustuqtop0  22257  metdsf  22864  metdsge  22865  mulc1cncf  22921  lebnumlem1  22973  cmetcaulem  23298  ovollb2lem  23469  ovolctb  23471  ovolunlem1a  23477  ovolunlem1  23478  ovoliunlem1  23483  ovoliunlem2  23484  ovoliun  23486  ovolshftlem1  23490  ovolscalem1  23494  ovolicc1  23497  ioombl1lem1  23539  uniioombllem2  23564  volsup2  23586  volcn  23587  vitalilem4  23592  vitalilem5  23593  mbfconst  23614  mbfmax  23630  mbfsup  23645  i1f1lem  23670  i1f1  23671  i1fres  23686  itg1climres  23695  itg2splitlem  23729  itg2split  23730  itg2monolem1  23731  itg2mono  23734  itg2i1fseq  23736  itg2i1fseq2  23737  dvreslem  23887  dvivthlem1  23985  dvfsumrlimf  24002  dvfsumlem3  24005  ftc1lem2  24013  ftc1lem6  24018  tdeglem1  24032  radcnvlem1  24381  pserulm  24390  psercn2  24391  abelthlem4  24402  efif1olem4  24506  lgamgulmlem6  24974  gamcvg  24996  basellem4  25024  basellem7  25027  basellem9  25029  lgsfcl2  25242  lgsqrlem2  25286  lgseisenlem1  25314  dchrmusum2  25397  dchrvmasumiflem1  25404  dchrisum0ff  25410  dchrisum0lem1b  25418  dchrisum0lem2a  25420  abvcxp  25518  padicabv  25533  axlowdimlem15  26050  crctcshwlkn0  26942  wlkiswwlks2lem5  27000  wlkswwlksf1o  27006  wlknwwlksnfunOLD  27015  wlkwwlkfunOLD  27023  wwlksnextfun  27035  clwlkclwwlklem2a  27141  clwlkclwwlkf  27151  clwwlkf  27196  clwlksfclwwlkOLD  27236  frgrncvvdeqlem4  27477  numclwwlk1lem2f  27534  numclwlk2lem2f  27557  numclwlk2lem2fOLD  27564  ipblnfi  28039  ubthlem1  28054  htthlem  28102  hlimadd  28378  chscllem1  28824  cnlnadjlem2  29255  strlem3a  29439  hstrlem3a  29447  xppreima2  29777  xrge0mulc1cn  30312  esumpcvgval  30465  esumcvg  30473  mbfmco2  30652  eulerpartlems  30747  erdszelem9  31504  cvmlift3lem3  31626  elmrsubrn  31740  mvhf  31778  iprodefisum  31949  unbdqndv1  32816  knoppf  32843  ftc1anclem3  33799  ftc1anclem5  33801  lflnegcl  34855  lshpkrcl  34896  tendo0cl  36571  binomcxplemradcnv  39051  binomcxplemcvg  39053  binomcxplemnotnn0  39055  rnmptc  39842  projf1o  39875  mullimc  40328  ellimcabssub0  40329  mullimcf  40335  constlimc  40336  idlimc  40338  neglimc  40359  addlimc  40360  0ellimcdiv  40361  fnlimf  40390  cncfshift  40567  icccncfext  40580  cncfiooiccre  40588  fprodsubrecnncnvlem  40601  fprodaddrecnncnvlem  40603  dvmptresicc  40614  ioodvbdlimc1lem1  40626  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  dvnxpaek  40637  dvnprodlem1  40641  itgsinexplem1  40649  itgiccshift  40675  dirkercncflem2  40800  fourierdlem4  40807  fourierdlem5  40808  fourierdlem9  40812  fourierdlem14  40817  fourierdlem16  40819  fourierdlem17  40820  fourierdlem18  40821  fourierdlem21  40824  fourierdlem22  40825  fourierdlem37  40840  fourierdlem50  40852  fourierdlem51  40853  fourierdlem53  40855  fourierdlem55  40857  fourierdlem57  40859  fourierdlem58  40860  fourierdlem59  40861  fourierdlem60  40862  fourierdlem61  40863  fourierdlem67  40869  fourierdlem68  40870  fourierdlem72  40874  fourierdlem73  40875  fourierdlem74  40876  fourierdlem75  40877  fourierdlem76  40878  fourierdlem78  40880  fourierdlem80  40882  fourierdlem81  40883  fourierdlem83  40885  fourierdlem84  40886  fourierdlem88  40890  fourierdlem92  40894  fourierdlem93  40895  fourierdlem97  40899  fourierdlem101  40903  fourierdlem103  40905  fourierdlem104  40906  fourierdlem111  40913  sqwvfoura  40924  elaa2lem  40929  etransclem1  40931  etransclem8  40938  etransclem20  40950  etransclem33  40963  etransclem35  40965  etransclem39  40969  rrxtopnfi  40985  ioorrnopnxrlem  41005  sge0tsms  41076  sge0snmpt  41079  sge0fsummpt  41086  sge0pr  41090  sge0lessmpt  41095  sge0iunmptlemfi  41109  sge0iunmptlemre  41111  sge0iunmpt  41114  sge0rpcpnf  41117  sge0isum  41123  nnfoctbdjlem  41151  psmeasure  41167  voliunsge0lem  41168  meaiuninclem  41176  meaiuninc3v  41180  meaiininclem  41182  omeiunltfirp  41215  carageniuncllem2  41218  caratheodorylem1  41222  caratheodorylem2  41223  isomenndlem  41226  hoicvr  41244  hoicvrrex  41252  ovnsupge0  41253  ovnlecvr  41254  ovnf  41259  ovn0lem  41261  ovnsubaddlem1  41266  ovnsubadd  41268  hsphoif  41272  sge0hsphoire  41285  hoidmv1lelem1  41287  hoidmv1lelem2  41288  hoidmv1lelem3  41289  hoidmv1le  41290  hoidmvlelem2  41292  hoidmvlelem3  41293  ovnhoilem1  41297  ovnsubadd2lem  41341  ovolval4lem1  41345  ovolval4lem2  41346  ovolval5lem2  41349  ovnovollem1  41352  ovnovollem2  41353  vonioolem2  41377  vonicclem2  41380  smfmbfcex  41450  smflim  41467  nsssmfmbflem  41468  smfmullem4  41483  smfsuplem1  41499  smfsuplem3  41501  smflimsuplem3  41510  fmtnodvds  42031  c0mgm  42477  c0mhm  42478  c0snmgmhm  42482  lincvalsc0  42778  lcoc0  42779  linc0scn0  42780  linc1  42782  lincscm  42787  lincresunit3  42838  amgmlemALT  43120
  Copyright terms: Public domain W3C validator