Theorem fmptd 7095

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142  ∀wral 3076   ↦ cmpt 5181  ⟶wf 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-fun 6523  df-fn 6524  df-f 6525

This theorem is referenced by:  fmpttd  7096  fnwelem  8111  fsetfcdm  8841  fdiagfn  8872  resixpfo  8918  xpmapenlem  9116  unxpdomlem3  9202  fsuppmptdm  9322  cantnfp1lem1  9633  cantnfp1lem2  9634  cantnfp1lem3  9635  cantnf  9648  updjudhf  9889  fseqenlem2  9981  dfac8clem  9988  coftr  10230  isf34lem2  10330  axcc2lem  10393  axdc2lem  10405  axdc3lem4  10410  pwcfsdom  10541  rpnnen1lem1  12979  tpf  14512  caucvg  15706  sumrblem  15738  summolem2a  15742  supcvg  15886  prodrblem  15959  prodmolem2a  15964  crth  16813  eulerthlem1  16816  prmreclem6  16957  4sqlem11  16991  vdwlem2  17018  vdwlem4  17020  vdwlem6  17022  vdwlem10  17026  ramub1lem2  17063  prmgaplcm  17096  frmdup1  18898  grpinvf  19028  mulgnngsum  19121  cycsubm  19243  cycsubgcl  19247  cycsubgss  19248  conjghm  19289  conjnmz  19292  qusghm  19295  galactghm  19444  symgextf  19457  symgfixf  19476  pmtrdifwrdellem1  19521  odf1  19602  dfod2  19604  pgpssslw  19654  frgpmhm  19805  gsummptfidmsplitres  19971  gsummptfidminv  19987  gsumzunsnd  19996  gsummpt1n0  20005  ablfac1b  20112  ablfac2  20131  c0mgm  20504  c0mhm  20505  c0snmgmhm  20507  abvtrivd  20878  issrngd  20901  pwssplit0  21122  rngqiprngimf  21364  mulgghm2  21525  frobrhm  21624  isphld  21703  pjff  21761  frlmup1  21847  asclf  21930  psr1cl  22009  evlslem1  22132  evlsval2  22137  evlsval3  22139  mplmapghm  22172  evlsmaprhm  22181  selvcllem5  22189  evls1maprhm  22436  rhmmpl  22440  scmatf  22586  mdetf  22652  maduf  22698  pmatcollpw3fi1lem1  22843  chfacfisf  22911  chfacfisfcpmat  22912  cpmidpmatlem2  22928  lly1stc  23553  txcnmpt  23681  txlm  23705  xkoinjcn  23744  kqffn  23782  txflf  24063  tsmsfbas  24185  ustuqtop0  24297  metdsf  24906  metdsge  24907  mulc1cncf  24964  lebnumlem1  25020  cmetcaulem  25347  ovollb2lem  25547  ovolctb  25549  ovolunlem1a  25555  ovolunlem1  25556  ovoliunlem1  25561  ovoliunlem2  25562  ovoliun  25564  ovolshftlem1  25568  ovolscalem1  25572  ovolicc1  25575  ioombl1lem1  25617  uniioombllem2  25642  volsup2  25664  volcn  25665  vitalilem4  25670  vitalilem5  25671  mbfconst  25692  mbfmax  25708  mbfsup  25723  i1f1lem  25748  i1f1  25749  i1fres  25764  itg1climres  25773  itg2splitlem  25807  itg2split  25808  itg2monolem1  25809  itg2mono  25812  itg2i1fseq  25814  itg2i1fseq2  25815  dvreslem  25968  dvmptresicc  25975  dvivthlem1  26067  dvfsumrlimf  26084  dvfsumlem3  26087  ftc1lem2  26095  ftc1lem6  26100  radcnvlem1  26473  pserulm  26482  psercn2  26483  abelthlem4  26494  efif1olem4  26607  lgamgulmlem6  27095  gamcvg  27117  basellem4  27145  basellem7  27148  basellem9  27150  lgsfcl2  27364  lgsqrlem2  27408  lgseisenlem1  27436  dchrmusum2  27555  dchrvmasumiflem1  27562  dchrisum0ff  27568  dchrisum0lem1b  27576  dchrisum0lem2a  27578  abvcxp  27676  padicabv  27691  axlowdimlem15  29154  crctcshwlkn0  30018  wlkiswwlks2lem5  30070  wlkswwlksf1o  30076  wwlksnextfun  30095  clwlkclwwlklem2a  30197  clwlkclwwlkf  30207  clwwlkf  30246  frgrncvvdeqlem4  30501  numclwwlk1lem2f  30554  numclwlk2lem2f  30576  ipblnfi  31055  ubthlem1  31070  htthlem  31117  hlimadd  31393  chscllem1  31837  cnlnadjlem2  32268  strlem3a  32452  hstrlem3a  32460  xppreima2  32850  suppovss  32880  fsuppcurry1  32923  fsuppcurry2  32924  pwrssmgc  33175  mndlactf1  33201  mndlactfo  33202  mndractf1  33203  mndractfo  33204  lmodvslmhm  33227  conjga  33347  rlocf1  33452  nsgmgc  33595  elrspunidl  33611  r1plmhm  33803  r1pquslmic  33804  selvply1rhmlem1  33814  mplvrpmga  33839  mplvrpmmhm  33840  mplvrpmrhm  33841  psrmonprod  33846  mplmonprod  33848  ply1degltdimlem  33916  ply1degltdim  33917  extdgfialglem1  33986  algextdeglem8  34018  rhmpreimacnlem  34178  rhmpreimacn  34179  xrge0mulc1cn  34235  esumpcvgval  34372  esumcvg  34380  mbfmco2  34559  eulerpartlems  34654  onvfowev  35456  erdszelem9  35546  cvmlift3lem3  35668  ex-sategoelel  35768  ex-sategoelelomsuc  35773  elmrsubrn  35867  mvhf  35905  iprodefisum  36088  unbdqndv1  36943  knoppf  36970  ftc1anclem3  38191  ftc1anclem5  38193  lflnegcl  39696  lshpkrcl  39737  tendo0cl  41411  primrootscoprf  42715  aks6d1c2p1  42732  aks6d1c4  42738  aks6d1c2lem4  42741  aks6d1c2  42744  aks6d1c5lem0  42749  aks6d1c5  42753  sticksstones2  42761  sticksstones8  42767  sticksstones9  42768  sticksstones10  42769  sticksstones11  42770  sticksstones12a  42771  sticksstones17  42777  sticksstones18  42778  aks6d1c6lem2  42785  aks6d1c6lem3  42786  aks6d1c6lem4  42787  aks6d1c6isolem1  42788  aks6d1c6isolem2  42789  aks6d1c6isolem3  42790  aks6d1c6lem5  42791  aks5lem2  42801  frlmsnic  43155  rhmpsr  43162  evlsbagval  43165  cantnfub  43895  binomcxplemradcnv  44925  binomcxplemcvg  44927  binomcxplemnotnn0  44929  projf1o  45771  mullimc  46189  ellimcabssub0  46190  mullimcf  46196  constlimc  46197  idlimc  46199  neglimc  46218  addlimc  46219  0ellimcdiv  46220  fnlimf  46249  liminfpnfuz  46387  xlimpnfxnegmnf2  46429  cncfshift  46445  icccncfext  46458  cncfiooiccre  46466  fprodsubrecnncnvlem  46478  fprodaddrecnncnvlem  46480  ioodvbdlimc1lem1  46502  ioodvbdlimc1lem2  46503  ioodvbdlimc2lem  46505  dvnxpaek  46513  dvnprodlem1  46517  itgsinexplem1  46525  itgiccshift  46551  dirkercncflem2  46675  fourierdlem4  46682  fourierdlem5  46683  fourierdlem9  46687  fourierdlem14  46692  fourierdlem16  46694  fourierdlem17  46695  fourierdlem18  46696  fourierdlem21  46699  fourierdlem22  46700  fourierdlem37  46715  fourierdlem50  46727  fourierdlem51  46728  fourierdlem53  46730  fourierdlem55  46732  fourierdlem57  46734  fourierdlem58  46735  fourierdlem59  46736  fourierdlem60  46737  fourierdlem61  46738  fourierdlem67  46744  fourierdlem68  46745  fourierdlem72  46749  fourierdlem73  46750  fourierdlem74  46751  fourierdlem75  46752  fourierdlem76  46753  fourierdlem78  46755  fourierdlem80  46757  fourierdlem81  46758  fourierdlem83  46760  fourierdlem84  46761  fourierdlem88  46765  fourierdlem92  46769  fourierdlem93  46770  fourierdlem97  46774  fourierdlem101  46778  fourierdlem103  46780  fourierdlem104  46781  fourierdlem111  46788  sqwvfoura  46799  elaa2lem  46804  etransclem1  46806  etransclem8  46813  etransclem20  46825  etransclem33  46838  etransclem35  46840  etransclem39  46844  rrxtopnfi  46858  ioorrnopnxrlem  46877  sge0tsms  46951  sge0snmpt  46954  sge0fsummpt  46961  sge0pr  46965  sge0lessmpt  46970  sge0iunmptlemfi  46984  sge0iunmptlemre  46986  sge0iunmpt  46989  sge0rpcpnf  46992  sge0isum  46998  nnfoctbdjlem  47026  psmeasure  47042  voliunsge0lem  47043  meaiuninclem  47051  meaiuninc3v  47055  meaiininclem  47057  omeiunltfirp  47090  carageniuncllem2  47093  caratheodorylem1  47097  caratheodorylem2  47098  isomenndlem  47101  hoicvrrex  47127  ovnsupge0  47128  ovnlecvr  47129  ovnf  47134  ovn0lem  47136  ovnsubaddlem1  47141  ovnsubadd  47143  hsphoif  47147  sge0hsphoire  47160  hoidmv1lelem1  47162  hoidmv1lelem2  47163  hoidmv1lelem3  47164  hoidmv1le  47165  hoidmvlelem2  47167  hoidmvlelem3  47168  ovnhoilem1  47172  ovnsubadd2lem  47216  ovolval4lem1  47220  ovolval4lem2  47221  ovolval5lem2  47224  ovnovollem1  47227  ovnovollem2  47228  vonioolem2  47252  vonicclem2  47255  smflim  47348  nsssmfmbflem  47349  smfmullem4  47365  smfsuplem1  47382  smfsuplem3  47384  smflimsuplem3  47393  fsetsnf  47642  cfsetsnfsetf  47649  cfsetsnfsetfo  47651  imasetpreimafvbijlemf  48004  prproropf1o  48110  fmtnodvds  48150  upgrimwlklem2  48517  isubgr3stgrlem6  48590  lincvalsc0  49040  lcoc0  49041  linc0scn0  49042  linc1  49044  lincscm  49049  lincresunit3  49100  1arympt1  49257  1arymaptf  49260  2arympt  49268  2arymaptf  49271  ackendofnn0  49303  amgmlemALT  50421