Theorem fmptd 7114

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 3147	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)
3		fmptd.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	fmpt 7110	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶)
5	2, 4	sylib 217	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062   ↦ cmpt 5232  ⟶wf 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-fun 6546  df-fn 6547  df-f 6548

This theorem is referenced by:  fmpttd  7115  rnmptcOLD  7209  fnwelem  8117  fsetfcdm  8854  fsetfocdm  8855  fdiagfn  8884  resixpfo  8930  xpmapenlem  9144  unxpdomlem3  9252  fsuppmptdm  9374  cantnfp1lem1  9673  cantnfp1lem2  9674  cantnfp1lem3  9675  cantnf  9688  updjudhf  9926  fseqenlem2  10020  dfac8clem  10027  coftr  10268  isf34lem2  10368  axcc2lem  10431  axdc2lem  10443  axdc3lem4  10448  pwcfsdom  10578  rpnnen1lem1  12962  caucvg  15625  sumrblem  15657  summolem2a  15661  supcvg  15802  prodrblem  15873  prodmolem2a  15878  crth  16711  eulerthlem1  16714  prmreclem6  16854  4sqlem11  16888  vdwlem2  16915  vdwlem4  16917  vdwlem6  16919  vdwlem10  16923  ramub1lem2  16960  prmgaplcm  16993  frmdup1  18745  grpinvf  18871  mulgnngsum  18959  cycsubm  19079  cycsubgcl  19083  cycsubgss  19084  conjghm  19123  conjnmz  19126  qusghm  19129  galactghm  19272  symgextf  19285  symgfixf  19304  pmtrdifwrdellem1  19349  odf1  19430  dfod2  19432  pgpssslw  19482  frgpmhm  19633  gsummptfidmsplitres  19799  gsummptfidminv  19815  gsumzunsnd  19824  gsummpt1n0  19833  ablfac1b  19940  ablfac2  19959  abvtrivd  20448  issrngd  20469  pwssplit0  20669  mulgghm2  21046  isphld  21207  pjff  21267  frlmup1  21353  asclf  21436  psr1cl  21522  evlslem1  21645  evlsval2  21650  scmatf  22031  mdetf  22097  maduf  22143  pmatcollpw3fi1lem1  22288  chfacfisf  22356  chfacfisfcpmat  22357  cpmidpmatlem2  22373  lly1stc  23000  txcnmpt  23128  txlm  23152  xkoinjcn  23191  kqffn  23229  txflf  23510  tsmsfbas  23632  ustuqtop0  23745  metdsf  24364  metdsge  24365  mulc1cncf  24421  lebnumlem1  24477  cmetcaulem  24805  ovollb2lem  25005  ovolctb  25007  ovolunlem1a  25013  ovolunlem1  25014  ovoliunlem1  25019  ovoliunlem2  25020  ovoliun  25022  ovolshftlem1  25026  ovolscalem1  25030  ovolicc1  25033  ioombl1lem1  25075  uniioombllem2  25100  volsup2  25122  volcn  25123  vitalilem4  25128  vitalilem5  25129  mbfconst  25150  mbfmax  25166  mbfsup  25181  i1f1lem  25206  i1f1  25207  i1fres  25223  itg1climres  25232  itg2splitlem  25266  itg2split  25267  itg2monolem1  25268  itg2mono  25271  itg2i1fseq  25273  itg2i1fseq2  25274  dvreslem  25426  dvmptresicc  25433  dvivthlem1  25525  dvfsumrlimf  25542  dvfsumlem3  25545  ftc1lem2  25553  ftc1lem6  25558  tdeglem1OLD  25574  radcnvlem1  25925  pserulm  25934  psercn2  25935  abelthlem4  25946  efif1olem4  26054  lgamgulmlem6  26538  gamcvg  26560  basellem4  26588  basellem7  26591  basellem9  26593  lgsfcl2  26806  lgsqrlem2  26850  lgseisenlem1  26878  dchrmusum2  26997  dchrvmasumiflem1  27004  dchrisum0ff  27010  dchrisum0lem1b  27018  dchrisum0lem2a  27020  abvcxp  27118  padicabv  27133  axlowdimlem15  28214  crctcshwlkn0  29075  wlkiswwlks2lem5  29127  wlkswwlksf1o  29133  wwlksnextfun  29152  clwlkclwwlklem2a  29251  clwlkclwwlkf  29261  clwwlkf  29300  frgrncvvdeqlem4  29555  numclwwlk1lem2f  29608  numclwlk2lem2f  29630  ipblnfi  30108  ubthlem1  30123  htthlem  30170  hlimadd  30446  chscllem1  30890  cnlnadjlem2  31321  strlem3a  31505  hstrlem3a  31513  xppreima2  31876  suppovss  31906  fsuppcurry1  31950  fsuppcurry2  31951  pwrssmgc  32170  lmodvslmhm  32202  frobrhm  32382  nsgmgc  32523  elrspunidl  32546  ply1degltdimlem  32707  ply1degltdim  32708  evls1maprhm  32759  rhmpreimacnlem  32864  rhmpreimacn  32865  xrge0mulc1cn  32921  esumpcvgval  33076  esumcvg  33084  mbfmco2  33264  eulerpartlems  33359  erdszelem9  34190  cvmlift3lem3  34312  ex-sategoelel  34412  ex-sategoelelomsuc  34417  elmrsubrn  34511  mvhf  34549  iprodefisum  34711  gg-psercn2  35178  unbdqndv1  35384  knoppf  35411  ftc1anclem3  36563  ftc1anclem5  36565  lflnegcl  37945  lshpkrcl  37986  tendo0cl  39661  aks6d1c2p1  40956  sticksstones2  40963  sticksstones8  40969  sticksstones9  40970  sticksstones10  40971  sticksstones11  40972  sticksstones12a  40973  sticksstones17  40979  sticksstones18  40980  metakunt1  40985  metakunt2  40986  metakunt19  41003  metakunt25  41009  frlmsnic  41110  rhmmpl  41125  mplmapghm  41128  evlsval3  41131  evlsbagval  41138  evlsmaprhm  41142  selvcllem5  41154  cantnfub  42071  binomcxplemradcnv  43111  binomcxplemcvg  43113  binomcxplemnotnn0  43115  projf1o  43896  mullimc  44332  ellimcabssub0  44333  mullimcf  44339  constlimc  44340  idlimc  44342  neglimc  44363  addlimc  44364  0ellimcdiv  44365  fnlimf  44394  liminfpnfuz  44532  xlimpnfxnegmnf2  44574  cncfshift  44590  icccncfext  44603  cncfiooiccre  44611  fprodsubrecnncnvlem  44623  fprodaddrecnncnvlem  44625  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnxpaek  44658  dvnprodlem1  44662  itgsinexplem1  44670  itgiccshift  44696  dirkercncflem2  44820  fourierdlem4  44827  fourierdlem5  44828  fourierdlem9  44832  fourierdlem14  44837  fourierdlem16  44839  fourierdlem17  44840  fourierdlem18  44841  fourierdlem21  44844  fourierdlem22  44845  fourierdlem37  44860  fourierdlem50  44872  fourierdlem51  44873  fourierdlem53  44875  fourierdlem55  44877  fourierdlem57  44879  fourierdlem58  44880  fourierdlem59  44881  fourierdlem60  44882  fourierdlem61  44883  fourierdlem67  44889  fourierdlem68  44890  fourierdlem72  44894  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem78  44900  fourierdlem80  44902  fourierdlem81  44903  fourierdlem83  44905  fourierdlem84  44906  fourierdlem88  44910  fourierdlem92  44914  fourierdlem93  44915  fourierdlem97  44919  fourierdlem101  44923  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  sqwvfoura  44944  elaa2lem  44949  etransclem1  44951  etransclem8  44958  etransclem20  44970  etransclem33  44983  etransclem35  44985  etransclem39  44989  rrxtopnfi  45003  ioorrnopnxrlem  45022  sge0tsms  45096  sge0snmpt  45099  sge0fsummpt  45106  sge0pr  45110  sge0lessmpt  45115  sge0iunmptlemfi  45129  sge0iunmptlemre  45131  sge0iunmpt  45134  sge0rpcpnf  45137  sge0isum  45143  nnfoctbdjlem  45171  psmeasure  45187  voliunsge0lem  45188  meaiuninclem  45196  meaiuninc3v  45200  meaiininclem  45202  omeiunltfirp  45235  carageniuncllem2  45238  caratheodorylem1  45242  caratheodorylem2  45243  isomenndlem  45246  hoicvr  45264  hoicvrrex  45272  ovnsupge0  45273  ovnlecvr  45274  ovnf  45279  ovn0lem  45281  ovnsubaddlem1  45286  ovnsubadd  45288  hsphoif  45292  sge0hsphoire  45305  hoidmv1lelem1  45307  hoidmv1lelem2  45308  hoidmv1lelem3  45309  hoidmv1le  45310  hoidmvlelem2  45312  hoidmvlelem3  45313  ovnhoilem1  45317  ovnsubadd2lem  45361  ovolval4lem1  45365  ovolval4lem2  45366  ovolval5lem2  45369  ovnovollem1  45372  ovnovollem2  45373  vonioolem2  45397  vonicclem2  45400  smflim  45493  nsssmfmbflem  45494  smfmullem4  45510  smfsuplem1  45527  smfsuplem3  45529  smflimsuplem3  45538  fsetsnf  45761  cfsetsnfsetf  45768  cfsetsnfsetfo  45770  imasetpreimafvbijlemf  46069  prproropf1o  46175  fmtnodvds  46212  c0mgm  46708  c0mhm  46709  c0snmgmhm  46713  rngqiprngimf  46782  lincvalsc0  47102  lcoc0  47103  linc0scn0  47104  linc1  47106  lincscm  47111  lincresunit3  47162  1arympt1  47324  1arymaptf  47327  2arympt  47335  2arymaptf  47338  ackendofnn0  47370  amgmlemALT  47850