Theorem fmptd 7068

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052   ↦ cmpt 5181  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  fmpttd  7069  fnwelem  8083  fsetfcdm  8809  fdiagfn  8840  resixpfo  8886  xpmapenlem  9084  unxpdomlem3  9170  fsuppmptdm  9291  cantnfp1lem1  9599  cantnfp1lem2  9600  cantnfp1lem3  9601  cantnf  9614  updjudhf  9855  fseqenlem2  9947  dfac8clem  9954  coftr  10195  isf34lem2  10295  axcc2lem  10358  axdc2lem  10370  axdc3lem4  10375  pwcfsdom  10506  rpnnen1lem1  12903  tpf  14434  caucvg  15614  sumrblem  15646  summolem2a  15650  supcvg  15791  prodrblem  15864  prodmolem2a  15869  crth  16717  eulerthlem1  16720  prmreclem6  16861  4sqlem11  16895  vdwlem2  16922  vdwlem4  16924  vdwlem6  16926  vdwlem10  16930  ramub1lem2  16967  prmgaplcm  17000  frmdup1  18801  grpinvf  18928  mulgnngsum  19021  cycsubm  19143  cycsubgcl  19147  cycsubgss  19148  conjghm  19190  conjnmz  19193  qusghm  19196  galactghm  19345  symgextf  19358  symgfixf  19377  pmtrdifwrdellem1  19422  odf1  19503  dfod2  19505  pgpssslw  19555  frgpmhm  19706  gsummptfidmsplitres  19872  gsummptfidminv  19888  gsumzunsnd  19897  gsummpt1n0  19906  ablfac1b  20013  ablfac2  20032  c0mgm  20407  c0mhm  20408  c0snmgmhm  20410  abvtrivd  20777  issrngd  20800  pwssplit0  21022  rngqiprngimf  21264  mulgghm2  21443  frobrhm  21542  isphld  21621  pjff  21679  frlmup1  21765  asclf  21849  psr1cl  21928  evlslem1  22049  evlsval2  22054  evlsval3  22056  evls1maprhm  22332  rhmmpl  22339  scmatf  22485  mdetf  22551  maduf  22597  pmatcollpw3fi1lem1  22742  chfacfisf  22810  chfacfisfcpmat  22811  cpmidpmatlem2  22827  lly1stc  23452  txcnmpt  23580  txlm  23604  xkoinjcn  23643  kqffn  23681  txflf  23962  tsmsfbas  24084  ustuqtop0  24196  metdsf  24805  metdsge  24806  mulc1cncf  24866  lebnumlem1  24928  cmetcaulem  25256  ovollb2lem  25457  ovolctb  25459  ovolunlem1a  25465  ovolunlem1  25466  ovoliunlem1  25471  ovoliunlem2  25472  ovoliun  25474  ovolshftlem1  25478  ovolscalem1  25482  ovolicc1  25485  ioombl1lem1  25527  uniioombllem2  25552  volsup2  25574  volcn  25575  vitalilem4  25580  vitalilem5  25581  mbfconst  25602  mbfmax  25618  mbfsup  25633  i1f1lem  25658  i1f1  25659  i1fres  25674  itg1climres  25683  itg2splitlem  25717  itg2split  25718  itg2monolem1  25719  itg2mono  25722  itg2i1fseq  25724  itg2i1fseq2  25725  dvreslem  25878  dvmptresicc  25885  dvivthlem1  25981  dvfsumrlimf  25999  dvfsumlem3  26003  ftc1lem2  26011  ftc1lem6  26016  radcnvlem1  26390  pserulm  26399  psercn2  26400  psercn2OLD  26401  abelthlem4  26412  efif1olem4  26522  lgamgulmlem6  27012  gamcvg  27034  basellem4  27062  basellem7  27065  basellem9  27067  lgsfcl2  27282  lgsqrlem2  27326  lgseisenlem1  27354  dchrmusum2  27473  dchrvmasumiflem1  27480  dchrisum0ff  27486  dchrisum0lem1b  27494  dchrisum0lem2a  27496  abvcxp  27594  padicabv  27609  axlowdimlem15  29041  crctcshwlkn0  29906  wlkiswwlks2lem5  29958  wlkswwlksf1o  29964  wwlksnextfun  29983  clwlkclwwlklem2a  30085  clwlkclwwlkf  30095  clwwlkf  30134  frgrncvvdeqlem4  30389  numclwwlk1lem2f  30442  numclwlk2lem2f  30464  ipblnfi  30943  ubthlem1  30958  htthlem  31005  hlimadd  31281  chscllem1  31725  cnlnadjlem2  32156  strlem3a  32340  hstrlem3a  32348  xppreima2  32741  suppovss  32771  fsuppcurry1  32814  fsuppcurry2  32815  pwrssmgc  33093  mndlactf1  33119  mndlactfo  33120  mndractf1  33121  mndractfo  33122  lmodvslmhm  33144  conjga  33264  rlocf1  33367  nsgmgc  33505  elrspunidl  33521  r1plmhm  33703  r1pquslmic  33704  mplvrpmga  33722  mplvrpmmhm  33723  mplvrpmrhm  33724  psrmonprod  33729  mplmonprod  33731  ply1degltdimlem  33800  ply1degltdim  33801  extdgfialglem1  33870  algextdeglem8  33902  rhmpreimacnlem  34062  rhmpreimacn  34063  xrge0mulc1cn  34119  esumpcvgval  34256  esumcvg  34264  mbfmco2  34443  eulerpartlems  34538  erdszelem9  35415  cvmlift3lem3  35537  ex-sategoelel  35637  ex-sategoelelomsuc  35642  elmrsubrn  35736  mvhf  35774  iprodefisum  35957  unbdqndv1  36730  knoppf  36757  ftc1anclem3  37946  ftc1anclem5  37948  lflnegcl  39451  lshpkrcl  39492  tendo0cl  41166  primrootscoprf  42471  aks6d1c2p1  42488  aks6d1c4  42494  aks6d1c2lem4  42497  aks6d1c2  42500  aks6d1c5lem0  42505  aks6d1c5  42509  sticksstones2  42517  sticksstones8  42523  sticksstones9  42524  sticksstones10  42525  sticksstones11  42526  sticksstones12a  42527  sticksstones17  42533  sticksstones18  42534  aks6d1c6lem2  42541  aks6d1c6lem3  42542  aks6d1c6lem4  42543  aks6d1c6isolem1  42544  aks6d1c6isolem2  42545  aks6d1c6isolem3  42546  aks6d1c6lem5  42547  aks5lem2  42557  frlmsnic  42910  rhmpsr  42920  mplmapghm  42922  evlsbagval  42927  evlsmaprhm  42931  selvcllem5  42940  cantnfub  43678  binomcxplemradcnv  44708  binomcxplemcvg  44710  binomcxplemnotnn0  44712  projf1o  45555  mullimc  45976  ellimcabssub0  45977  mullimcf  45983  constlimc  45984  idlimc  45986  neglimc  46005  addlimc  46006  0ellimcdiv  46007  fnlimf  46036  liminfpnfuz  46174  xlimpnfxnegmnf2  46216  cncfshift  46232  icccncfext  46245  cncfiooiccre  46253  fprodsubrecnncnvlem  46265  fprodaddrecnncnvlem  46267  ioodvbdlimc1lem1  46289  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  dvnxpaek  46300  dvnprodlem1  46304  itgsinexplem1  46312  itgiccshift  46338  dirkercncflem2  46462  fourierdlem4  46469  fourierdlem5  46470  fourierdlem9  46474  fourierdlem14  46479  fourierdlem16  46481  fourierdlem17  46482  fourierdlem18  46483  fourierdlem21  46486  fourierdlem22  46487  fourierdlem37  46502  fourierdlem50  46514  fourierdlem51  46515  fourierdlem53  46517  fourierdlem55  46519  fourierdlem57  46521  fourierdlem58  46522  fourierdlem59  46523  fourierdlem60  46524  fourierdlem61  46525  fourierdlem67  46531  fourierdlem68  46532  fourierdlem72  46536  fourierdlem73  46537  fourierdlem74  46538  fourierdlem75  46539  fourierdlem76  46540  fourierdlem78  46542  fourierdlem80  46544  fourierdlem81  46545  fourierdlem83  46547  fourierdlem84  46548  fourierdlem88  46552  fourierdlem92  46556  fourierdlem93  46557  fourierdlem97  46561  fourierdlem101  46565  fourierdlem103  46567  fourierdlem104  46568  fourierdlem111  46575  sqwvfoura  46586  elaa2lem  46591  etransclem1  46593  etransclem8  46600  etransclem20  46612  etransclem33  46625  etransclem35  46627  etransclem39  46631  rrxtopnfi  46645  ioorrnopnxrlem  46664  sge0tsms  46738  sge0snmpt  46741  sge0fsummpt  46748  sge0pr  46752  sge0lessmpt  46757  sge0iunmptlemfi  46771  sge0iunmptlemre  46773  sge0iunmpt  46776  sge0rpcpnf  46779  sge0isum  46785  nnfoctbdjlem  46813  psmeasure  46829  voliunsge0lem  46830  meaiuninclem  46838  meaiuninc3v  46842  meaiininclem  46844  omeiunltfirp  46877  carageniuncllem2  46880  caratheodorylem1  46884  caratheodorylem2  46885  isomenndlem  46888  hoicvr  46906  hoicvrrex  46914  ovnsupge0  46915  ovnlecvr  46916  ovnf  46921  ovn0lem  46923  ovnsubaddlem1  46928  ovnsubadd  46930  hsphoif  46934  sge0hsphoire  46947  hoidmv1lelem1  46949  hoidmv1lelem2  46950  hoidmv1lelem3  46951  hoidmv1le  46952  hoidmvlelem2  46954  hoidmvlelem3  46955  ovnhoilem1  46959  ovnsubadd2lem  47003  ovolval4lem1  47007  ovolval4lem2  47008  ovolval5lem2  47011  ovnovollem1  47014  ovnovollem2  47015  vonioolem2  47039  vonicclem2  47042  smflim  47135  nsssmfmbflem  47136  smfmullem4  47152  smfsuplem1  47169  smfsuplem3  47171  smflimsuplem3  47180  fsetsnf  47411  cfsetsnfsetf  47418  cfsetsnfsetfo  47420  imasetpreimafvbijlemf  47761  prproropf1o  47867  fmtnodvds  47904  upgrimwlklem2  48258  isubgr3stgrlem6  48331  lincvalsc0  48781  lcoc0  48782  linc0scn0  48783  linc1  48785  lincscm  48790  lincresunit3  48841  1arympt1  48998  1arymaptf  49001  2arympt  49009  2arymaptf  49012  ackendofnn0  49044  amgmlemALT  50162