Theorem fmptd 7148

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∀wral 3067   ↦ cmpt 5249  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-fun 6575  df-fn 6576  df-f 6577

This theorem is referenced by:  fmpttd  7149  fnwelem  8172  fsetfcdm  8918  fdiagfn  8948  resixpfo  8994  xpmapenlem  9210  unxpdomlem3  9315  fsuppmptdm  9445  cantnfp1lem1  9747  cantnfp1lem2  9748  cantnfp1lem3  9749  cantnf  9762  updjudhf  10000  fseqenlem2  10094  dfac8clem  10101  coftr  10342  isf34lem2  10442  axcc2lem  10505  axdc2lem  10517  axdc3lem4  10522  pwcfsdom  10652  rpnnen1lem1  13043  tpf  14548  caucvg  15727  sumrblem  15759  summolem2a  15763  supcvg  15904  prodrblem  15977  prodmolem2a  15982  crth  16825  eulerthlem1  16828  prmreclem6  16968  4sqlem11  17002  vdwlem2  17029  vdwlem4  17031  vdwlem6  17033  vdwlem10  17037  ramub1lem2  17074  prmgaplcm  17107  frmdup1  18899  grpinvf  19026  mulgnngsum  19119  cycsubm  19242  cycsubgcl  19246  cycsubgss  19247  conjghm  19289  conjnmz  19292  qusghm  19295  galactghm  19446  symgextf  19459  symgfixf  19478  pmtrdifwrdellem1  19523  odf1  19604  dfod2  19606  pgpssslw  19656  frgpmhm  19807  gsummptfidmsplitres  19973  gsummptfidminv  19989  gsumzunsnd  19998  gsummpt1n0  20007  ablfac1b  20114  ablfac2  20133  c0mgm  20485  c0mhm  20486  c0snmgmhm  20488  abvtrivd  20855  issrngd  20878  pwssplit0  21080  rngqiprngimf  21330  mulgghm2  21510  frobrhm  21617  isphld  21695  pjff  21755  frlmup1  21841  asclf  21925  psr1cl  22004  evlslem1  22129  evlsval2  22134  evls1maprhm  22401  rhmmpl  22408  scmatf  22556  mdetf  22622  maduf  22668  pmatcollpw3fi1lem1  22813  chfacfisf  22881  chfacfisfcpmat  22882  cpmidpmatlem2  22898  lly1stc  23525  txcnmpt  23653  txlm  23677  xkoinjcn  23716  kqffn  23754  txflf  24035  tsmsfbas  24157  ustuqtop0  24270  metdsf  24889  metdsge  24890  mulc1cncf  24950  lebnumlem1  25012  cmetcaulem  25341  ovollb2lem  25542  ovolctb  25544  ovolunlem1a  25550  ovolunlem1  25551  ovoliunlem1  25556  ovoliunlem2  25557  ovoliun  25559  ovolshftlem1  25563  ovolscalem1  25567  ovolicc1  25570  ioombl1lem1  25612  uniioombllem2  25637  volsup2  25659  volcn  25660  vitalilem4  25665  vitalilem5  25666  mbfconst  25687  mbfmax  25703  mbfsup  25718  i1f1lem  25743  i1f1  25744  i1fres  25760  itg1climres  25769  itg2splitlem  25803  itg2split  25804  itg2monolem1  25805  itg2mono  25808  itg2i1fseq  25810  itg2i1fseq2  25811  dvreslem  25964  dvmptresicc  25971  dvivthlem1  26067  dvfsumrlimf  26085  dvfsumlem3  26089  ftc1lem2  26097  ftc1lem6  26102  radcnvlem1  26474  pserulm  26483  psercn2  26484  psercn2OLD  26485  abelthlem4  26496  efif1olem4  26605  lgamgulmlem6  27095  gamcvg  27117  basellem4  27145  basellem7  27148  basellem9  27150  lgsfcl2  27365  lgsqrlem2  27409  lgseisenlem1  27437  dchrmusum2  27556  dchrvmasumiflem1  27563  dchrisum0ff  27569  dchrisum0lem1b  27577  dchrisum0lem2a  27579  abvcxp  27677  padicabv  27692  axlowdimlem15  28989  crctcshwlkn0  29854  wlkiswwlks2lem5  29906  wlkswwlksf1o  29912  wwlksnextfun  29931  clwlkclwwlklem2a  30030  clwlkclwwlkf  30040  clwwlkf  30079  frgrncvvdeqlem4  30334  numclwwlk1lem2f  30387  numclwlk2lem2f  30409  ipblnfi  30887  ubthlem1  30902  htthlem  30949  hlimadd  31225  chscllem1  31669  cnlnadjlem2  32100  strlem3a  32284  hstrlem3a  32292  xppreima2  32669  suppovss  32697  fsuppcurry1  32739  fsuppcurry2  32740  pwrssmgc  32973  mndlactf1  33012  mndlactfo  33013  mndractf1  33014  mndractfo  33015  lmodvslmhm  33033  rlocf1  33245  nsgmgc  33405  elrspunidl  33421  r1plmhm  33595  r1pquslmic  33596  ply1degltdimlem  33635  ply1degltdim  33636  algextdeglem8  33715  rhmpreimacnlem  33830  rhmpreimacn  33831  xrge0mulc1cn  33887  esumpcvgval  34042  esumcvg  34050  mbfmco2  34230  eulerpartlems  34325  erdszelem9  35167  cvmlift3lem3  35289  ex-sategoelel  35389  ex-sategoelelomsuc  35394  elmrsubrn  35488  mvhf  35526  iprodefisum  35703  unbdqndv1  36474  knoppf  36501  ftc1anclem3  37655  ftc1anclem5  37657  lflnegcl  39031  lshpkrcl  39072  tendo0cl  40747  primrootscoprf  42058  aks6d1c2p1  42075  aks6d1c4  42081  aks6d1c2lem4  42084  aks6d1c2  42087  aks6d1c5lem0  42092  aks6d1c5  42096  sticksstones2  42104  sticksstones8  42110  sticksstones9  42111  sticksstones10  42112  sticksstones11  42113  sticksstones12a  42114  sticksstones17  42120  sticksstones18  42121  aks6d1c6lem2  42128  aks6d1c6lem3  42129  aks6d1c6lem4  42130  aks6d1c6isolem1  42131  aks6d1c6isolem2  42132  aks6d1c6isolem3  42133  aks6d1c6lem5  42134  aks5lem2  42144  metakunt1  42162  metakunt2  42163  metakunt19  42180  metakunt25  42186  frlmsnic  42495  rhmpsr  42507  mplmapghm  42511  evlsval3  42514  evlsbagval  42521  evlsmaprhm  42525  selvcllem5  42537  cantnfub  43283  binomcxplemradcnv  44321  binomcxplemcvg  44323  binomcxplemnotnn0  44325  projf1o  45104  mullimc  45537  ellimcabssub0  45538  mullimcf  45544  constlimc  45545  idlimc  45547  neglimc  45568  addlimc  45569  0ellimcdiv  45570  fnlimf  45599  liminfpnfuz  45737  xlimpnfxnegmnf2  45779  cncfshift  45795  icccncfext  45808  cncfiooiccre  45816  fprodsubrecnncnvlem  45828  fprodaddrecnncnvlem  45830  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnxpaek  45863  dvnprodlem1  45867  itgsinexplem1  45875  itgiccshift  45901  dirkercncflem2  46025  fourierdlem4  46032  fourierdlem5  46033  fourierdlem9  46037  fourierdlem14  46042  fourierdlem16  46044  fourierdlem17  46045  fourierdlem18  46046  fourierdlem21  46049  fourierdlem22  46050  fourierdlem37  46065  fourierdlem50  46077  fourierdlem51  46078  fourierdlem53  46080  fourierdlem55  46082  fourierdlem57  46084  fourierdlem58  46085  fourierdlem59  46086  fourierdlem60  46087  fourierdlem61  46088  fourierdlem67  46094  fourierdlem68  46095  fourierdlem72  46099  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem78  46105  fourierdlem80  46107  fourierdlem81  46108  fourierdlem83  46110  fourierdlem84  46111  fourierdlem88  46115  fourierdlem92  46119  fourierdlem93  46120  fourierdlem97  46124  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  sqwvfoura  46149  elaa2lem  46154  etransclem1  46156  etransclem8  46163  etransclem20  46175  etransclem33  46188  etransclem35  46190  etransclem39  46194  rrxtopnfi  46208  ioorrnopnxrlem  46227  sge0tsms  46301  sge0snmpt  46304  sge0fsummpt  46311  sge0pr  46315  sge0lessmpt  46320  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0iunmpt  46339  sge0rpcpnf  46342  sge0isum  46348  nnfoctbdjlem  46376  psmeasure  46392  voliunsge0lem  46393  meaiuninclem  46401  meaiuninc3v  46405  meaiininclem  46407  omeiunltfirp  46440  carageniuncllem2  46443  caratheodorylem1  46447  caratheodorylem2  46448  isomenndlem  46451  hoicvr  46469  hoicvrrex  46477  ovnsupge0  46478  ovnlecvr  46479  ovnf  46484  ovn0lem  46486  ovnsubaddlem1  46491  ovnsubadd  46493  hsphoif  46497  sge0hsphoire  46510  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmv1le  46515  hoidmvlelem2  46517  hoidmvlelem3  46518  ovnhoilem1  46522  ovnsubadd2lem  46566  ovolval4lem1  46570  ovolval4lem2  46571  ovolval5lem2  46574  ovnovollem1  46577  ovnovollem2  46578  vonioolem2  46602  vonicclem2  46605  smflim  46698  nsssmfmbflem  46699  smfmullem4  46715  smfsuplem1  46732  smfsuplem3  46734  smflimsuplem3  46743  fsetsnf  46966  cfsetsnfsetf  46973  cfsetsnfsetfo  46975  imasetpreimafvbijlemf  47275  prproropf1o  47381  fmtnodvds  47418  lincvalsc0  48150  lcoc0  48151  linc0scn0  48152  linc1  48154  lincscm  48159  lincresunit3  48210  1arympt1  48372  1arymaptf  48375  2arympt  48383  2arymaptf  48386  ackendofnn0  48418  amgmlemALT  48897