Theorem fmptd 6970

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

Step	Hyp	Ref	Expression
1		fmptd.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
2	1	ralrimiva 3107	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)
3		fmptd.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	fmpt 6966	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶)
5	2, 4	sylib 217	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063   ↦ cmpt 5153  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-fun 6420  df-fn 6421  df-f 6422

This theorem is referenced by:  fmpttd  6971  rnmptcOLD  7065  fnwelem  7943  fsetfcdm  8606  fsetfocdm  8607  fdiagfn  8636  resixpfo  8682  xpmapenlem  8880  unxpdomlem3  8958  fsuppmptdm  9069  cantnfp1lem1  9366  cantnfp1lem2  9367  cantnfp1lem3  9368  cantnf  9381  updjudhf  9620  fseqenlem2  9712  dfac8clem  9719  coftr  9960  isf34lem2  10060  axcc2lem  10123  axdc2lem  10135  axdc3lem4  10140  pwcfsdom  10270  rpnnen1lem1  12647  caucvg  15318  sumrblem  15351  summolem2a  15355  supcvg  15496  prodrblem  15567  prodmolem2a  15572  crth  16407  eulerthlem1  16410  prmreclem6  16550  4sqlem11  16584  vdwlem2  16611  vdwlem4  16613  vdwlem6  16615  vdwlem10  16619  ramub1lem2  16656  prmgaplcm  16689  frmdup1  18418  grpinvf  18541  mulgnngsum  18624  cycsubm  18736  cycsubgcl  18740  cycsubgss  18741  conjghm  18780  conjnmz  18783  qusghm  18786  galactghm  18927  symgextf  18940  symgfixf  18959  pmtrdifwrdellem1  19004  odf1  19084  dfod2  19086  pgpssslw  19134  frgpmhm  19286  gsummptfidmsplitres  19447  gsummptfidminv  19463  gsumzunsnd  19472  gsummpt1n0  19481  ablfac1b  19588  ablfac2  19607  abvtrivd  20015  issrngd  20036  pwssplit0  20235  mulgghm2  20610  isphld  20771  pjff  20829  frlmup1  20915  asclf  20996  psr1cl  21081  evlslem1  21202  evlsval2  21207  scmatf  21586  mdetf  21652  maduf  21698  pmatcollpw3fi1lem1  21843  chfacfisf  21911  chfacfisfcpmat  21912  cpmidpmatlem2  21928  lly1stc  22555  txcnmpt  22683  txlm  22707  xkoinjcn  22746  kqffn  22784  txflf  23065  tsmsfbas  23187  ustuqtop0  23300  metdsf  23917  metdsge  23918  mulc1cncf  23974  lebnumlem1  24030  cmetcaulem  24357  ovollb2lem  24557  ovolctb  24559  ovolunlem1a  24565  ovolunlem1  24566  ovoliunlem1  24571  ovoliunlem2  24572  ovoliun  24574  ovolshftlem1  24578  ovolscalem1  24582  ovolicc1  24585  ioombl1lem1  24627  uniioombllem2  24652  volsup2  24674  volcn  24675  vitalilem4  24680  vitalilem5  24681  mbfconst  24702  mbfmax  24718  mbfsup  24733  i1f1lem  24758  i1f1  24759  i1fres  24775  itg1climres  24784  itg2splitlem  24818  itg2split  24819  itg2monolem1  24820  itg2mono  24823  itg2i1fseq  24825  itg2i1fseq2  24826  dvreslem  24978  dvmptresicc  24985  dvivthlem1  25077  dvfsumrlimf  25094  dvfsumlem3  25097  ftc1lem2  25105  ftc1lem6  25110  tdeglem1OLD  25126  radcnvlem1  25477  pserulm  25486  psercn2  25487  abelthlem4  25498  efif1olem4  25606  lgamgulmlem6  26088  gamcvg  26110  basellem4  26138  basellem7  26141  basellem9  26143  lgsfcl2  26356  lgsqrlem2  26400  lgseisenlem1  26428  dchrmusum2  26547  dchrvmasumiflem1  26554  dchrisum0ff  26560  dchrisum0lem1b  26568  dchrisum0lem2a  26570  abvcxp  26668  padicabv  26683  axlowdimlem15  27227  crctcshwlkn0  28087  wlkiswwlks2lem5  28139  wlkswwlksf1o  28145  wwlksnextfun  28164  clwlkclwwlklem2a  28263  clwlkclwwlkf  28273  clwwlkf  28312  frgrncvvdeqlem4  28567  numclwwlk1lem2f  28620  numclwlk2lem2f  28642  ipblnfi  29118  ubthlem1  29133  htthlem  29180  hlimadd  29456  chscllem1  29900  cnlnadjlem2  30331  strlem3a  30515  hstrlem3a  30523  xppreima2  30889  suppovss  30919  fsuppcurry1  30962  fsuppcurry2  30963  pwrssmgc  31180  lmodvslmhm  31212  frobrhm  31387  nsgmgc  31499  elrspunidl  31508  rhmpreimacnlem  31736  rhmpreimacn  31737  xrge0mulc1cn  31793  esumpcvgval  31946  esumcvg  31954  mbfmco2  32132  eulerpartlems  32227  erdszelem9  33061  cvmlift3lem3  33183  ex-sategoelel  33283  ex-sategoelelomsuc  33288  elmrsubrn  33382  mvhf  33420  iprodefisum  33613  unbdqndv1  34615  knoppf  34642  ftc1anclem3  35779  ftc1anclem5  35781  lflnegcl  37016  lshpkrcl  37057  tendo0cl  38731  sticksstones2  40031  sticksstones8  40037  sticksstones9  40038  sticksstones10  40039  sticksstones11  40040  sticksstones12a  40041  sticksstones17  40047  sticksstones18  40048  metakunt1  40053  metakunt2  40054  metakunt19  40071  metakunt25  40077  selvval2lem5  40155  frlmsnic  40188  evlsval3  40195  evlsbagval  40198  binomcxplemradcnv  41859  binomcxplemcvg  41861  binomcxplemnotnn0  41863  projf1o  42625  mullimc  43047  ellimcabssub0  43048  mullimcf  43054  constlimc  43055  idlimc  43057  neglimc  43078  addlimc  43079  0ellimcdiv  43080  fnlimf  43109  liminfpnfuz  43247  xlimpnfxnegmnf2  43289  cncfshift  43305  icccncfext  43318  cncfiooiccre  43326  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnxpaek  43373  dvnprodlem1  43377  itgsinexplem1  43385  itgiccshift  43411  dirkercncflem2  43535  fourierdlem4  43542  fourierdlem5  43543  fourierdlem9  43547  fourierdlem14  43552  fourierdlem16  43554  fourierdlem17  43555  fourierdlem18  43556  fourierdlem21  43559  fourierdlem22  43560  fourierdlem37  43575  fourierdlem50  43587  fourierdlem51  43588  fourierdlem53  43590  fourierdlem55  43592  fourierdlem57  43594  fourierdlem58  43595  fourierdlem59  43596  fourierdlem60  43597  fourierdlem61  43598  fourierdlem67  43604  fourierdlem68  43605  fourierdlem72  43609  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem78  43615  fourierdlem80  43617  fourierdlem81  43618  fourierdlem83  43620  fourierdlem84  43621  fourierdlem88  43625  fourierdlem92  43629  fourierdlem93  43630  fourierdlem97  43634  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  sqwvfoura  43659  elaa2lem  43664  etransclem1  43666  etransclem8  43673  etransclem20  43685  etransclem33  43698  etransclem35  43700  etransclem39  43704  rrxtopnfi  43718  ioorrnopnxrlem  43737  sge0tsms  43808  sge0snmpt  43811  sge0fsummpt  43818  sge0pr  43822  sge0lessmpt  43827  sge0iunmptlemfi  43841  sge0iunmptlemre  43843  sge0iunmpt  43846  sge0rpcpnf  43849  sge0isum  43855  nnfoctbdjlem  43883  psmeasure  43899  voliunsge0lem  43900  meaiuninclem  43908  meaiuninc3v  43912  meaiininclem  43914  omeiunltfirp  43947  carageniuncllem2  43950  caratheodorylem1  43954  caratheodorylem2  43955  isomenndlem  43958  hoicvr  43976  hoicvrrex  43984  ovnsupge0  43985  ovnlecvr  43986  ovnf  43991  ovn0lem  43993  ovnsubaddlem1  43998  ovnsubadd  44000  hsphoif  44004  sge0hsphoire  44017  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmv1le  44022  hoidmvlelem2  44024  hoidmvlelem3  44025  ovnhoilem1  44029  ovnsubadd2lem  44073  ovolval4lem1  44077  ovolval4lem2  44078  ovolval5lem2  44081  ovnovollem1  44084  ovnovollem2  44085  vonioolem2  44109  vonicclem2  44112  smflim  44199  nsssmfmbflem  44200  smfmullem4  44215  smfsuplem1  44231  smfsuplem3  44233  smflimsuplem3  44242  fsetsnf  44432  cfsetsnfsetf  44439  cfsetsnfsetfo  44441  imasetpreimafvbijlemf  44741  prproropf1o  44847  fmtnodvds  44884  c0mgm  45355  c0mhm  45356  c0snmgmhm  45360  lincvalsc0  45650  lcoc0  45651  linc0scn0  45652  linc1  45654  lincscm  45659  lincresunit3  45710  1arympt1  45872  1arymaptf  45875  2arympt  45883  2arymaptf  45886  ackendofnn0  45918  amgmlemALT  46393