Theorem fmptd 7115

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3050   ↦ cmpt 5207  ⟶wf 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pr 5414

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-nul 4316  df-if 4508  df-sn 4609  df-pr 4611  df-op 4615  df-br 5126  df-opab 5188  df-mpt 5208  df-id 5560  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-fun 6544  df-fn 6545  df-f 6546

This theorem is referenced by:  fmpttd  7116  fnwelem  8139  fsetfcdm  8883  fdiagfn  8913  resixpfo  8959  xpmapenlem  9167  unxpdomlem3  9271  fsuppmptdm  9399  cantnfp1lem1  9701  cantnfp1lem2  9702  cantnfp1lem3  9703  cantnf  9716  updjudhf  9954  fseqenlem2  10048  dfac8clem  10055  coftr  10296  isf34lem2  10396  axcc2lem  10459  axdc2lem  10471  axdc3lem4  10476  pwcfsdom  10606  rpnnen1lem1  13003  tpf  14521  caucvg  15698  sumrblem  15730  summolem2a  15734  supcvg  15875  prodrblem  15948  prodmolem2a  15953  crth  16798  eulerthlem1  16801  prmreclem6  16942  4sqlem11  16976  vdwlem2  17003  vdwlem4  17005  vdwlem6  17007  vdwlem10  17011  ramub1lem2  17048  prmgaplcm  17081  frmdup1  18851  grpinvf  18978  mulgnngsum  19071  cycsubm  19194  cycsubgcl  19198  cycsubgss  19199  conjghm  19241  conjnmz  19244  qusghm  19247  galactghm  19395  symgextf  19408  symgfixf  19427  pmtrdifwrdellem1  19472  odf1  19553  dfod2  19555  pgpssslw  19605  frgpmhm  19756  gsummptfidmsplitres  19922  gsummptfidminv  19938  gsumzunsnd  19947  gsummpt1n0  19956  ablfac1b  20063  ablfac2  20082  c0mgm  20432  c0mhm  20433  c0snmgmhm  20435  abvtrivd  20806  issrngd  20829  pwssplit0  21030  rngqiprngimf  21274  mulgghm2  21454  frobrhm  21561  isphld  21639  pjff  21699  frlmup1  21785  asclf  21869  psr1cl  21948  evlslem1  22073  evlsval2  22078  evls1maprhm  22347  rhmmpl  22354  scmatf  22502  mdetf  22568  maduf  22614  pmatcollpw3fi1lem1  22759  chfacfisf  22827  chfacfisfcpmat  22828  cpmidpmatlem2  22844  lly1stc  23469  txcnmpt  23597  txlm  23621  xkoinjcn  23660  kqffn  23698  txflf  23979  tsmsfbas  24101  ustuqtop0  24214  metdsf  24825  metdsge  24826  mulc1cncf  24886  lebnumlem1  24948  cmetcaulem  25277  ovollb2lem  25478  ovolctb  25480  ovolunlem1a  25486  ovolunlem1  25487  ovoliunlem1  25492  ovoliunlem2  25493  ovoliun  25495  ovolshftlem1  25499  ovolscalem1  25503  ovolicc1  25506  ioombl1lem1  25548  uniioombllem2  25573  volsup2  25595  volcn  25596  vitalilem4  25601  vitalilem5  25602  mbfconst  25623  mbfmax  25639  mbfsup  25654  i1f1lem  25679  i1f1  25680  i1fres  25695  itg1climres  25704  itg2splitlem  25738  itg2split  25739  itg2monolem1  25740  itg2mono  25743  itg2i1fseq  25745  itg2i1fseq2  25746  dvreslem  25899  dvmptresicc  25906  dvivthlem1  26002  dvfsumrlimf  26020  dvfsumlem3  26024  ftc1lem2  26032  ftc1lem6  26037  radcnvlem1  26411  pserulm  26420  psercn2  26421  psercn2OLD  26422  abelthlem4  26433  efif1olem4  26542  lgamgulmlem6  27032  gamcvg  27054  basellem4  27082  basellem7  27085  basellem9  27087  lgsfcl2  27302  lgsqrlem2  27346  lgseisenlem1  27374  dchrmusum2  27493  dchrvmasumiflem1  27500  dchrisum0ff  27506  dchrisum0lem1b  27514  dchrisum0lem2a  27516  abvcxp  27614  padicabv  27629  axlowdimlem15  28920  crctcshwlkn0  29788  wlkiswwlks2lem5  29840  wlkswwlksf1o  29846  wwlksnextfun  29865  clwlkclwwlklem2a  29964  clwlkclwwlkf  29974  clwwlkf  30013  frgrncvvdeqlem4  30268  numclwwlk1lem2f  30321  numclwlk2lem2f  30343  ipblnfi  30821  ubthlem1  30836  htthlem  30883  hlimadd  31159  chscllem1  31603  cnlnadjlem2  32034  strlem3a  32218  hstrlem3a  32226  xppreima2  32608  suppovss  32637  fsuppcurry1  32683  fsuppcurry2  32684  pwrssmgc  32936  mndlactf1  32977  mndlactfo  32978  mndractf1  32979  mndractfo  32980  lmodvslmhm  32999  rlocf1  33223  nsgmgc  33381  elrspunidl  33397  r1plmhm  33571  r1pquslmic  33572  ply1degltdimlem  33614  ply1degltdim  33615  algextdeglem8  33706  rhmpreimacnlem  33824  rhmpreimacn  33825  xrge0mulc1cn  33881  esumpcvgval  34020  esumcvg  34028  mbfmco2  34208  eulerpartlems  34303  erdszelem9  35145  cvmlift3lem3  35267  ex-sategoelel  35367  ex-sategoelelomsuc  35372  elmrsubrn  35466  mvhf  35504  iprodefisum  35682  unbdqndv1  36450  knoppf  36477  ftc1anclem3  37643  ftc1anclem5  37645  lflnegcl  39017  lshpkrcl  39058  tendo0cl  40733  primrootscoprf  42043  aks6d1c2p1  42060  aks6d1c4  42066  aks6d1c2lem4  42069  aks6d1c2  42072  aks6d1c5lem0  42077  aks6d1c5  42081  sticksstones2  42089  sticksstones8  42095  sticksstones9  42096  sticksstones10  42097  sticksstones11  42098  sticksstones12a  42099  sticksstones17  42105  sticksstones18  42106  aks6d1c6lem2  42113  aks6d1c6lem3  42114  aks6d1c6lem4  42115  aks6d1c6isolem1  42116  aks6d1c6isolem2  42117  aks6d1c6isolem3  42118  aks6d1c6lem5  42119  aks5lem2  42129  metakunt1  42147  metakunt2  42148  metakunt19  42165  metakunt25  42171  frlmsnic  42495  rhmpsr  42507  mplmapghm  42511  evlsval3  42514  evlsbagval  42521  evlsmaprhm  42525  selvcllem5  42537  cantnfub  43279  binomcxplemradcnv  44316  binomcxplemcvg  44318  binomcxplemnotnn0  44320  projf1o  45147  mullimc  45576  ellimcabssub0  45577  mullimcf  45583  constlimc  45584  idlimc  45586  neglimc  45607  addlimc  45608  0ellimcdiv  45609  fnlimf  45638  liminfpnfuz  45776  xlimpnfxnegmnf2  45818  cncfshift  45834  icccncfext  45847  cncfiooiccre  45855  fprodsubrecnncnvlem  45867  fprodaddrecnncnvlem  45869  ioodvbdlimc1lem1  45891  ioodvbdlimc1lem2  45892  ioodvbdlimc2lem  45894  dvnxpaek  45902  dvnprodlem1  45906  itgsinexplem1  45914  itgiccshift  45940  dirkercncflem2  46064  fourierdlem4  46071  fourierdlem5  46072  fourierdlem9  46076  fourierdlem14  46081  fourierdlem16  46083  fourierdlem17  46084  fourierdlem18  46085  fourierdlem21  46088  fourierdlem22  46089  fourierdlem37  46104  fourierdlem50  46116  fourierdlem51  46117  fourierdlem53  46119  fourierdlem55  46121  fourierdlem57  46123  fourierdlem58  46124  fourierdlem59  46125  fourierdlem60  46126  fourierdlem61  46127  fourierdlem67  46133  fourierdlem68  46134  fourierdlem72  46138  fourierdlem73  46139  fourierdlem74  46140  fourierdlem75  46141  fourierdlem76  46142  fourierdlem78  46144  fourierdlem80  46146  fourierdlem81  46147  fourierdlem83  46149  fourierdlem84  46150  fourierdlem88  46154  fourierdlem92  46158  fourierdlem93  46159  fourierdlem97  46163  fourierdlem101  46167  fourierdlem103  46169  fourierdlem104  46170  fourierdlem111  46177  sqwvfoura  46188  elaa2lem  46193  etransclem1  46195  etransclem8  46202  etransclem20  46214  etransclem33  46227  etransclem35  46229  etransclem39  46233  rrxtopnfi  46247  ioorrnopnxrlem  46266  sge0tsms  46340  sge0snmpt  46343  sge0fsummpt  46350  sge0pr  46354  sge0lessmpt  46359  sge0iunmptlemfi  46373  sge0iunmptlemre  46375  sge0iunmpt  46378  sge0rpcpnf  46381  sge0isum  46387  nnfoctbdjlem  46415  psmeasure  46431  voliunsge0lem  46432  meaiuninclem  46440  meaiuninc3v  46444  meaiininclem  46446  omeiunltfirp  46479  carageniuncllem2  46482  caratheodorylem1  46486  caratheodorylem2  46487  isomenndlem  46490  hoicvr  46508  hoicvrrex  46516  ovnsupge0  46517  ovnlecvr  46518  ovnf  46523  ovn0lem  46525  ovnsubaddlem1  46530  ovnsubadd  46532  hsphoif  46536  sge0hsphoire  46549  hoidmv1lelem1  46551  hoidmv1lelem2  46552  hoidmv1lelem3  46553  hoidmv1le  46554  hoidmvlelem2  46556  hoidmvlelem3  46557  ovnhoilem1  46561  ovnsubadd2lem  46605  ovolval4lem1  46609  ovolval4lem2  46610  ovolval5lem2  46613  ovnovollem1  46616  ovnovollem2  46617  vonioolem2  46641  vonicclem2  46644  smflim  46737  nsssmfmbflem  46738  smfmullem4  46754  smfsuplem1  46771  smfsuplem3  46773  smflimsuplem3  46782  fsetsnf  47009  cfsetsnfsetf  47016  cfsetsnfsetfo  47018  imasetpreimafvbijlemf  47334  prproropf1o  47440  fmtnodvds  47477  isubgr3stgrlem6  47884  lincvalsc0  48284  lcoc0  48285  linc0scn0  48286  linc1  48288  lincscm  48293  lincresunit3  48344  1arympt1  48505  1arymaptf  48508  2arympt  48516  2arymaptf  48519  ackendofnn0  48551  amgmlemALT  49318