Theorem fmptd 6931

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2110  ∀wral 3061   ↦ cmpt 5135  ⟶wf 6376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-fun 6382  df-fn 6383  df-f 6384

This theorem is referenced by:  fmpttd  6932  rnmptcOLD  7023  fnwelem  7898  fsetfcdm  8541  fsetfocdm  8542  fdiagfn  8571  resixpfo  8617  xpmapenlem  8813  unxpdomlem3  8884  fsuppmptdm  8996  cantnfp1lem1  9293  cantnfp1lem2  9294  cantnfp1lem3  9295  cantnf  9308  updjudhf  9547  fseqenlem2  9639  dfac8clem  9646  coftr  9887  isf34lem2  9987  axcc2lem  10050  axdc2lem  10062  axdc3lem4  10067  pwcfsdom  10197  rpnnen1lem1  12574  caucvg  15242  sumrblem  15275  summolem2a  15279  supcvg  15420  prodrblem  15491  prodmolem2a  15496  crth  16331  eulerthlem1  16334  prmreclem6  16474  4sqlem11  16508  vdwlem2  16535  vdwlem4  16537  vdwlem6  16539  vdwlem10  16543  ramub1lem2  16580  prmgaplcm  16613  frmdup1  18291  grpinvf  18414  mulgnngsum  18497  cycsubm  18609  cycsubgcl  18613  cycsubgss  18614  conjghm  18653  conjnmz  18656  qusghm  18659  galactghm  18796  symgextf  18809  symgfixf  18828  pmtrdifwrdellem1  18873  odf1  18953  dfod2  18955  pgpssslw  19003  frgpmhm  19155  gsummptfidmsplitres  19316  gsummptfidminv  19332  gsumzunsnd  19341  gsummpt1n0  19350  ablfac1b  19457  ablfac2  19476  abvtrivd  19876  issrngd  19897  pwssplit0  20095  mulgghm2  20463  isphld  20616  pjff  20674  frlmup1  20760  asclf  20841  psr1cl  20927  evlslem1  21042  evlsval2  21047  scmatf  21426  mdetf  21492  maduf  21538  pmatcollpw3fi1lem1  21683  chfacfisf  21751  chfacfisfcpmat  21752  cpmidpmatlem2  21768  lly1stc  22393  txcnmpt  22521  txlm  22545  xkoinjcn  22584  kqffn  22622  txflf  22903  tsmsfbas  23025  ustuqtop0  23138  metdsf  23745  metdsge  23746  mulc1cncf  23802  lebnumlem1  23858  cmetcaulem  24185  ovollb2lem  24385  ovolctb  24387  ovolunlem1a  24393  ovolunlem1  24394  ovoliunlem1  24399  ovoliunlem2  24400  ovoliun  24402  ovolshftlem1  24406  ovolscalem1  24410  ovolicc1  24413  ioombl1lem1  24455  uniioombllem2  24480  volsup2  24502  volcn  24503  vitalilem4  24508  vitalilem5  24509  mbfconst  24530  mbfmax  24546  mbfsup  24561  i1f1lem  24586  i1f1  24587  i1fres  24603  itg1climres  24612  itg2splitlem  24646  itg2split  24647  itg2monolem1  24648  itg2mono  24651  itg2i1fseq  24653  itg2i1fseq2  24654  dvreslem  24806  dvmptresicc  24813  dvivthlem1  24905  dvfsumrlimf  24922  dvfsumlem3  24925  ftc1lem2  24933  ftc1lem6  24938  tdeglem1OLD  24954  radcnvlem1  25305  pserulm  25314  psercn2  25315  abelthlem4  25326  efif1olem4  25434  lgamgulmlem6  25916  gamcvg  25938  basellem4  25966  basellem7  25969  basellem9  25971  lgsfcl2  26184  lgsqrlem2  26228  lgseisenlem1  26256  dchrmusum2  26375  dchrvmasumiflem1  26382  dchrisum0ff  26388  dchrisum0lem1b  26396  dchrisum0lem2a  26398  abvcxp  26496  padicabv  26511  axlowdimlem15  27047  crctcshwlkn0  27905  wlkiswwlks2lem5  27957  wlkswwlksf1o  27963  wwlksnextfun  27982  clwlkclwwlklem2a  28081  clwlkclwwlkf  28091  clwwlkf  28130  frgrncvvdeqlem4  28385  numclwwlk1lem2f  28438  numclwlk2lem2f  28460  ipblnfi  28936  ubthlem1  28951  htthlem  28998  hlimadd  29274  chscllem1  29718  cnlnadjlem2  30149  strlem3a  30333  hstrlem3a  30341  xppreima2  30707  suppovss  30737  fsuppcurry1  30780  fsuppcurry2  30781  pwrssmgc  30997  lmodvslmhm  31029  frobrhm  31204  nsgmgc  31311  elrspunidl  31320  rhmpreimacnlem  31548  rhmpreimacn  31549  xrge0mulc1cn  31605  esumpcvgval  31758  esumcvg  31766  mbfmco2  31944  eulerpartlems  32039  erdszelem9  32874  cvmlift3lem3  32996  ex-sategoelel  33096  ex-sategoelelomsuc  33101  elmrsubrn  33195  mvhf  33233  iprodefisum  33425  unbdqndv1  34425  knoppf  34452  ftc1anclem3  35589  ftc1anclem5  35591  lflnegcl  36826  lshpkrcl  36867  tendo0cl  38541  sticksstones2  39825  sticksstones8  39831  sticksstones9  39832  sticksstones10  39833  sticksstones11  39834  sticksstones12a  39835  sticksstones17  39841  sticksstones18  39842  metakunt1  39847  metakunt2  39848  metakunt19  39865  metakunt25  39871  selvval2lem5  39942  frlmsnic  39975  evlsval3  39982  evlsbagval  39985  binomcxplemradcnv  41643  binomcxplemcvg  41645  binomcxplemnotnn0  41647  projf1o  42409  mullimc  42832  ellimcabssub0  42833  mullimcf  42839  constlimc  42840  idlimc  42842  neglimc  42863  addlimc  42864  0ellimcdiv  42865  fnlimf  42894  liminfpnfuz  43032  xlimpnfxnegmnf2  43074  cncfshift  43090  icccncfext  43103  cncfiooiccre  43111  fprodsubrecnncnvlem  43123  fprodaddrecnncnvlem  43125  ioodvbdlimc1lem1  43147  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  dvnxpaek  43158  dvnprodlem1  43162  itgsinexplem1  43170  itgiccshift  43196  dirkercncflem2  43320  fourierdlem4  43327  fourierdlem5  43328  fourierdlem9  43332  fourierdlem14  43337  fourierdlem16  43339  fourierdlem17  43340  fourierdlem18  43341  fourierdlem21  43344  fourierdlem22  43345  fourierdlem37  43360  fourierdlem50  43372  fourierdlem51  43373  fourierdlem53  43375  fourierdlem55  43377  fourierdlem57  43379  fourierdlem58  43380  fourierdlem59  43381  fourierdlem60  43382  fourierdlem61  43383  fourierdlem67  43389  fourierdlem68  43390  fourierdlem72  43394  fourierdlem73  43395  fourierdlem74  43396  fourierdlem75  43397  fourierdlem76  43398  fourierdlem78  43400  fourierdlem80  43402  fourierdlem81  43403  fourierdlem83  43405  fourierdlem84  43406  fourierdlem88  43410  fourierdlem92  43414  fourierdlem93  43415  fourierdlem97  43419  fourierdlem101  43423  fourierdlem103  43425  fourierdlem104  43426  fourierdlem111  43433  sqwvfoura  43444  elaa2lem  43449  etransclem1  43451  etransclem8  43458  etransclem20  43470  etransclem33  43483  etransclem35  43485  etransclem39  43489  rrxtopnfi  43503  ioorrnopnxrlem  43522  sge0tsms  43593  sge0snmpt  43596  sge0fsummpt  43603  sge0pr  43607  sge0lessmpt  43612  sge0iunmptlemfi  43626  sge0iunmptlemre  43628  sge0iunmpt  43631  sge0rpcpnf  43634  sge0isum  43640  nnfoctbdjlem  43668  psmeasure  43684  voliunsge0lem  43685  meaiuninclem  43693  meaiuninc3v  43697  meaiininclem  43699  omeiunltfirp  43732  carageniuncllem2  43735  caratheodorylem1  43739  caratheodorylem2  43740  isomenndlem  43743  hoicvr  43761  hoicvrrex  43769  ovnsupge0  43770  ovnlecvr  43771  ovnf  43776  ovn0lem  43778  ovnsubaddlem1  43783  ovnsubadd  43785  hsphoif  43789  sge0hsphoire  43802  hoidmv1lelem1  43804  hoidmv1lelem2  43805  hoidmv1lelem3  43806  hoidmv1le  43807  hoidmvlelem2  43809  hoidmvlelem3  43810  ovnhoilem1  43814  ovnsubadd2lem  43858  ovolval4lem1  43862  ovolval4lem2  43863  ovolval5lem2  43866  ovnovollem1  43869  ovnovollem2  43870  vonioolem2  43894  vonicclem2  43897  smflim  43984  nsssmfmbflem  43985  smfmullem4  44000  smfsuplem1  44016  smfsuplem3  44018  smflimsuplem3  44027  fsetsnf  44217  cfsetsnfsetf  44224  cfsetsnfsetfo  44226  imasetpreimafvbijlemf  44526  prproropf1o  44632  fmtnodvds  44669  c0mgm  45140  c0mhm  45141  c0snmgmhm  45145  lincvalsc0  45435  lcoc0  45436  linc0scn0  45437  linc1  45439  lincscm  45444  lincresunit3  45495  1arympt1  45657  1arymaptf  45660  2arympt  45668  2arymaptf  45671  ackendofnn0  45703  amgmlemALT  46178