Theorem fmptd 7110

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085   ↦ cmpt 5196  ⟶wf 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-fun 6539  df-fn 6540  df-f 6541

This theorem is referenced by:  fmpttd  7111  fnwelem  8126  fsetfcdm  8856  fdiagfn  8887  resixpfo  8933  xpmapenlem  9131  unxpdomlem3  9217  fsuppmptdm  9335  cantnfp1lem1  9646  cantnfp1lem2  9647  cantnfp1lem3  9648  cantnf  9661  updjudhf  9916  fseqenlem2  10008  dfac8clem  10015  coftr  10256  isf34lem2  10356  axcc2lem  10419  axdc2lem  10431  axdc3lem4  10436  pwcfsdom  10567  rpnnen1lem1  13001  tpf  14535  caucvg  15729  sumrblem  15761  summolem2a  15765  supcvg  15909  prodrblem  15982  prodmolem2a  15987  crth  16836  eulerthlem1  16839  prmreclem6  16980  4sqlem11  17014  vdwlem2  17041  vdwlem4  17043  vdwlem6  17045  vdwlem10  17049  ramub1lem2  17086  prmgaplcm  17119  frmdup1  18922  grpinvf  19052  mulgnngsum  19144  cycsubm  19272  cycsubgcl  19276  cycsubgss  19277  conjghm  19318  conjnmz  19321  qusghm  19324  galactghm  19473  symgextf  19486  symgfixf  19505  pmtrdifwrdellem1  19550  odf1  19631  dfod2  19633  pgpssslw  19683  frgpmhm  19834  gsummptfidmsplitres  20000  gsummptfidminv  20016  gsumzunsnd  20025  gsummpt1n0  20034  ablfac1b  20141  ablfac2  20160  c0mgm  20540  c0mhm  20541  c0snmgmhm  20543  abvtrivd  20912  issrngd  20935  pwssplit0  21156  rngqiprngimf  21407  mulgghm2  21594  frobrhm  21693  isphld  21772  pjff  21830  frlmup1  21916  asclf  21999  psr1cl  22078  evlslem1  22201  evlsval2  22206  evlsval3  22208  mplmapghm  22241  evlsmaprhm  22250  selvcllem5  22258  evls1maprhm  22504  rhmmpl  22508  scmatf  22654  mdetf  22720  maduf  22766  pmatcollpw3fi1lem1  22911  chfacfisf  22979  chfacfisfcpmat  22980  cpmidpmatlem2  22996  lly1stc  23621  txcnmpt  23749  txlm  23773  xkoinjcn  23812  kqffn  23850  txflf  24131  tsmsfbas  24253  ustuqtop0  24365  metdsf  24974  metdsge  24975  mulc1cncf  25032  lebnumlem1  25088  cmetcaulem  25415  ovollb2lem  25615  ovolctb  25617  ovolunlem1a  25623  ovolunlem1  25624  ovoliunlem1  25629  ovoliunlem2  25630  ovoliun  25632  ovolshftlem1  25636  ovolscalem1  25640  ovolicc1  25643  ioombl1lem1  25685  uniioombllem2  25710  volsup2  25732  volcn  25733  vitalilem4  25738  vitalilem5  25739  mbfconst  25760  mbfmax  25776  mbfsup  25791  i1f1lem  25816  i1f1  25817  i1fres  25832  itg1climres  25841  itg2splitlem  25875  itg2split  25876  itg2monolem1  25877  itg2mono  25880  itg2i1fseq  25882  itg2i1fseq2  25883  dvreslem  26036  dvmptresicc  26043  dvivthlem1  26135  dvfsumrlimf  26152  dvfsumlem3  26155  ftc1lem2  26163  ftc1lem6  26168  radcnvlem1  26541  pserulm  26550  psercn2  26551  abelthlem4  26562  efif1olem4  26675  lgamgulmlem6  27163  gamcvg  27185  basellem4  27213  basellem7  27216  basellem9  27218  lgsfcl2  27432  lgsqrlem2  27476  lgseisenlem1  27504  dchrmusum2  27623  dchrvmasumiflem1  27630  dchrisum0ff  27636  dchrisum0lem1b  27644  dchrisum0lem2a  27646  abvcxp  27744  padicabv  27759  axlowdimlem15  29246  crctcshwlkn0  30110  wlkiswwlks2lem5  30162  wlkswwlksf1o  30168  wwlksnextfun  30187  clwlkclwwlklem2a  30289  clwlkclwwlkf  30299  clwwlkf  30338  frgrncvvdeqlem4  30593  numclwwlk1lem2f  30646  numclwlk2lem2f  30668  ipblnfi  31147  ubthlem1  31162  htthlem  31209  hlimadd  31485  chscllem1  31929  cnlnadjlem2  32360  strlem3a  32544  hstrlem3a  32552  xppreima2  32936  suppovss  32966  fsuppcurry1  33009  fsuppcurry2  33010  pwrssmgc  33260  mndlactf1  33286  mndlactfo  33287  mndractf1  33288  mndractfo  33289  lmodvslmhm  33310  conjga  33430  rlocf1  33534  nsgmgc  33664  elrspunidl  33679  r1plmhm  33843  r1pquslmic  33844  selvply1rhmlem1  33854  mplvrpmga  33879  mplvrpmmhm  33880  mplvrpmrhm  33881  psrmonprod  33886  mplmonprod  33888  ply1degltdimlem  33956  ply1degltdim  33957  extdgfialglem1  34026  algextdeglem8  34058  rhmpreimacnlem  34218  rhmpreimacn  34219  xrge0mulc1cn  34275  esumpcvgval  34412  esumcvg  34420  mbfmco2  34599  eulerpartlems  34694  onvfowev  35498  erdszelem9  35589  cvmlift3lem3  35711  ex-sategoelel  35811  ex-sategoelelomsuc  35816  elmrsubrn  35910  mvhf  35948  iprodefisum  36131  unbdqndv1  36985  knoppf  37012  ftc1anclem3  38233  ftc1anclem5  38235  lflnegcl  39738  lshpkrcl  39779  tendo0cl  41453  primrootscoprf  42757  aks6d1c2p1  42774  aks6d1c4  42780  aks6d1c2lem4  42783  aks6d1c2  42786  aks6d1c5lem0  42791  aks6d1c5  42795  sticksstones2  42803  sticksstones8  42809  sticksstones9  42810  sticksstones10  42811  sticksstones11  42812  sticksstones12a  42813  sticksstones17  42819  sticksstones18  42820  aks6d1c6lem2  42827  aks6d1c6lem3  42828  aks6d1c6lem4  42829  aks6d1c6isolem1  42830  aks6d1c6isolem2  42831  aks6d1c6isolem3  42832  aks6d1c6lem5  42833  aks5lem2  42843  frlmsnic  43199  rhmpsr  43206  evlsbagval  43209  cantnfub  43939  binomcxplemradcnv  44953  binomcxplemcvg  44955  binomcxplemnotnn0  44957  projf1o  45805  mullimc  46223  ellimcabssub0  46224  mullimcf  46230  constlimc  46231  idlimc  46233  neglimc  46252  addlimc  46253  0ellimcdiv  46254  fnlimf  46283  liminfpnfuz  46421  xlimpnfxnegmnf2  46463  cncfshift  46479  icccncfext  46492  cncfiooiccre  46500  fprodsubrecnncnvlem  46512  fprodaddrecnncnvlem  46514  ioodvbdlimc1lem1  46536  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  dvnxpaek  46547  dvnprodlem1  46551  itgsinexplem1  46559  itgiccshift  46585  dirkercncflem2  46709  fourierdlem4  46716  fourierdlem5  46717  fourierdlem9  46721  fourierdlem14  46726  fourierdlem16  46728  fourierdlem17  46729  fourierdlem18  46730  fourierdlem21  46733  fourierdlem22  46734  fourierdlem37  46749  fourierdlem50  46761  fourierdlem51  46762  fourierdlem53  46764  fourierdlem55  46766  fourierdlem57  46768  fourierdlem58  46769  fourierdlem59  46770  fourierdlem60  46771  fourierdlem61  46772  fourierdlem67  46778  fourierdlem68  46779  fourierdlem72  46783  fourierdlem73  46784  fourierdlem74  46785  fourierdlem75  46786  fourierdlem76  46787  fourierdlem78  46789  fourierdlem80  46791  fourierdlem81  46792  fourierdlem83  46794  fourierdlem84  46795  fourierdlem88  46799  fourierdlem92  46803  fourierdlem93  46804  fourierdlem97  46808  fourierdlem101  46812  fourierdlem103  46814  fourierdlem104  46815  fourierdlem111  46822  sqwvfoura  46833  elaa2lem  46838  etransclem1  46840  etransclem8  46847  etransclem20  46859  etransclem33  46872  etransclem35  46874  etransclem39  46878  rrxtopnfi  46892  ioorrnopnxrlem  46911  sge0tsms  46985  sge0snmpt  46988  sge0fsummpt  46995  sge0pr  46999  sge0lessmpt  47004  sge0iunmptlemfi  47018  sge0iunmptlemre  47020  sge0iunmpt  47023  sge0rpcpnf  47026  sge0isum  47032  nnfoctbdjlem  47060  psmeasure  47076  voliunsge0lem  47077  meaiuninclem  47085  meaiuninc3v  47089  meaiininclem  47091  omeiunltfirp  47124  carageniuncllem2  47127  caratheodorylem1  47131  caratheodorylem2  47132  isomenndlem  47135  hoicvrrex  47161  ovnsupge0  47162  ovnlecvr  47163  ovnf  47168  ovn0lem  47170  ovnsubaddlem1  47175  ovnsubadd  47177  hsphoif  47181  sge0hsphoire  47194  hoidmv1lelem1  47196  hoidmv1lelem2  47197  hoidmv1lelem3  47198  hoidmv1le  47199  hoidmvlelem2  47201  hoidmvlelem3  47202  ovnhoilem1  47206  ovnsubadd2lem  47250  ovolval4lem1  47254  ovolval4lem2  47255  ovolval5lem2  47258  ovnovollem1  47261  ovnovollem2  47262  vonioolem2  47286  vonicclem2  47289  smflim  47382  nsssmfmbflem  47383  smfmullem4  47399  smfsuplem1  47416  smfsuplem3  47418  smflimsuplem3  47427  fsetsnf  47676  cfsetsnfsetf  47683  cfsetsnfsetfo  47685  imasetpreimafvbijlemf  48038  prproropf1o  48144  fmtnodvds  48184  upgrimwlklem2  48551  isubgr3stgrlem6  48624  lincvalsc0  49085  lcoc0  49086  linc0scn0  49087  linc1  49089  lincscm  49094  lincresunit3  49145  1arympt1  49302  1arymaptf  49305  2arympt  49313  2arymaptf  49316  ackendofnn0  49348  amgmlemALT  50476