Theorem fmptd 7048

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044   ↦ cmpt 5173  ⟶wf 6478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-fun 6484  df-fn 6485  df-f 6486

This theorem is referenced by:  fmpttd  7049  fnwelem  8064  fsetfcdm  8787  fdiagfn  8817  resixpfo  8863  xpmapenlem  9061  unxpdomlem3  9147  fsuppmptdm  9266  cantnfp1lem1  9574  cantnfp1lem2  9575  cantnfp1lem3  9576  cantnf  9589  updjudhf  9827  fseqenlem2  9919  dfac8clem  9926  coftr  10167  isf34lem2  10267  axcc2lem  10330  axdc2lem  10342  axdc3lem4  10347  pwcfsdom  10477  rpnnen1lem1  12879  tpf  14406  caucvg  15586  sumrblem  15618  summolem2a  15622  supcvg  15763  prodrblem  15836  prodmolem2a  15841  crth  16689  eulerthlem1  16692  prmreclem6  16833  4sqlem11  16867  vdwlem2  16894  vdwlem4  16896  vdwlem6  16898  vdwlem10  16902  ramub1lem2  16939  prmgaplcm  16972  frmdup1  18738  grpinvf  18865  mulgnngsum  18958  cycsubm  19081  cycsubgcl  19085  cycsubgss  19086  conjghm  19128  conjnmz  19131  qusghm  19134  galactghm  19283  symgextf  19296  symgfixf  19315  pmtrdifwrdellem1  19360  odf1  19441  dfod2  19443  pgpssslw  19493  frgpmhm  19644  gsummptfidmsplitres  19810  gsummptfidminv  19826  gsumzunsnd  19835  gsummpt1n0  19844  ablfac1b  19951  ablfac2  19970  c0mgm  20344  c0mhm  20345  c0snmgmhm  20347  abvtrivd  20717  issrngd  20740  pwssplit0  20962  rngqiprngimf  21204  mulgghm2  21383  frobrhm  21482  isphld  21561  pjff  21619  frlmup1  21705  asclf  21789  psr1cl  21868  evlslem1  21987  evlsval2  21992  evls1maprhm  22261  rhmmpl  22268  scmatf  22414  mdetf  22480  maduf  22526  pmatcollpw3fi1lem1  22671  chfacfisf  22739  chfacfisfcpmat  22740  cpmidpmatlem2  22756  lly1stc  23381  txcnmpt  23509  txlm  23533  xkoinjcn  23572  kqffn  23610  txflf  23891  tsmsfbas  24013  ustuqtop0  24126  metdsf  24735  metdsge  24736  mulc1cncf  24796  lebnumlem1  24858  cmetcaulem  25186  ovollb2lem  25387  ovolctb  25389  ovolunlem1a  25395  ovolunlem1  25396  ovoliunlem1  25401  ovoliunlem2  25402  ovoliun  25404  ovolshftlem1  25408  ovolscalem1  25412  ovolicc1  25415  ioombl1lem1  25457  uniioombllem2  25482  volsup2  25504  volcn  25505  vitalilem4  25510  vitalilem5  25511  mbfconst  25532  mbfmax  25548  mbfsup  25563  i1f1lem  25588  i1f1  25589  i1fres  25604  itg1climres  25613  itg2splitlem  25647  itg2split  25648  itg2monolem1  25649  itg2mono  25652  itg2i1fseq  25654  itg2i1fseq2  25655  dvreslem  25808  dvmptresicc  25815  dvivthlem1  25911  dvfsumrlimf  25929  dvfsumlem3  25933  ftc1lem2  25941  ftc1lem6  25946  radcnvlem1  26320  pserulm  26329  psercn2  26330  psercn2OLD  26331  abelthlem4  26342  efif1olem4  26452  lgamgulmlem6  26942  gamcvg  26964  basellem4  26992  basellem7  26995  basellem9  26997  lgsfcl2  27212  lgsqrlem2  27256  lgseisenlem1  27284  dchrmusum2  27403  dchrvmasumiflem1  27410  dchrisum0ff  27416  dchrisum0lem1b  27424  dchrisum0lem2a  27426  abvcxp  27524  padicabv  27539  axlowdimlem15  28901  crctcshwlkn0  29766  wlkiswwlks2lem5  29818  wlkswwlksf1o  29824  wwlksnextfun  29843  clwlkclwwlklem2a  29942  clwlkclwwlkf  29952  clwwlkf  29991  frgrncvvdeqlem4  30246  numclwwlk1lem2f  30299  numclwlk2lem2f  30321  ipblnfi  30799  ubthlem1  30814  htthlem  30861  hlimadd  31137  chscllem1  31581  cnlnadjlem2  32012  strlem3a  32196  hstrlem3a  32204  xppreima2  32594  suppovss  32623  fsuppcurry1  32668  fsuppcurry2  32669  pwrssmgc  32942  mndlactf1  32980  mndlactfo  32981  mndractf1  32982  mndractfo  32983  lmodvslmhm  33003  conjga  33112  rlocf1  33213  nsgmgc  33349  elrspunidl  33365  r1plmhm  33542  r1pquslmic  33543  mplvrpmga  33546  ply1degltdimlem  33589  ply1degltdim  33590  extdgfialglem1  33659  algextdeglem8  33691  rhmpreimacnlem  33851  rhmpreimacn  33852  xrge0mulc1cn  33908  esumpcvgval  34045  esumcvg  34053  mbfmco2  34233  eulerpartlems  34328  erdszelem9  35172  cvmlift3lem3  35294  ex-sategoelel  35394  ex-sategoelelomsuc  35399  elmrsubrn  35493  mvhf  35531  iprodefisum  35714  unbdqndv1  36482  knoppf  36509  ftc1anclem3  37675  ftc1anclem5  37677  lflnegcl  39054  lshpkrcl  39095  tendo0cl  40769  primrootscoprf  42074  aks6d1c2p1  42091  aks6d1c4  42097  aks6d1c2lem4  42100  aks6d1c2  42103  aks6d1c5lem0  42108  aks6d1c5  42112  sticksstones2  42120  sticksstones8  42126  sticksstones9  42127  sticksstones10  42128  sticksstones11  42129  sticksstones12a  42130  sticksstones17  42136  sticksstones18  42137  aks6d1c6lem2  42144  aks6d1c6lem3  42145  aks6d1c6lem4  42146  aks6d1c6isolem1  42147  aks6d1c6isolem2  42148  aks6d1c6isolem3  42149  aks6d1c6lem5  42150  aks5lem2  42160  frlmsnic  42513  rhmpsr  42525  mplmapghm  42529  evlsval3  42532  evlsbagval  42539  evlsmaprhm  42543  selvcllem5  42555  cantnfub  43294  binomcxplemradcnv  44325  binomcxplemcvg  44327  binomcxplemnotnn0  44329  projf1o  45175  mullimc  45597  ellimcabssub0  45598  mullimcf  45604  constlimc  45605  idlimc  45607  neglimc  45628  addlimc  45629  0ellimcdiv  45630  fnlimf  45659  liminfpnfuz  45797  xlimpnfxnegmnf2  45839  cncfshift  45855  icccncfext  45868  cncfiooiccre  45876  fprodsubrecnncnvlem  45888  fprodaddrecnncnvlem  45890  ioodvbdlimc1lem1  45912  ioodvbdlimc1lem2  45913  ioodvbdlimc2lem  45915  dvnxpaek  45923  dvnprodlem1  45927  itgsinexplem1  45935  itgiccshift  45961  dirkercncflem2  46085  fourierdlem4  46092  fourierdlem5  46093  fourierdlem9  46097  fourierdlem14  46102  fourierdlem16  46104  fourierdlem17  46105  fourierdlem18  46106  fourierdlem21  46109  fourierdlem22  46110  fourierdlem37  46125  fourierdlem50  46137  fourierdlem51  46138  fourierdlem53  46140  fourierdlem55  46142  fourierdlem57  46144  fourierdlem58  46145  fourierdlem59  46146  fourierdlem60  46147  fourierdlem61  46148  fourierdlem67  46154  fourierdlem68  46155  fourierdlem72  46159  fourierdlem73  46160  fourierdlem74  46161  fourierdlem75  46162  fourierdlem76  46163  fourierdlem78  46165  fourierdlem80  46167  fourierdlem81  46168  fourierdlem83  46170  fourierdlem84  46171  fourierdlem88  46175  fourierdlem92  46179  fourierdlem93  46180  fourierdlem97  46184  fourierdlem101  46188  fourierdlem103  46190  fourierdlem104  46191  fourierdlem111  46198  sqwvfoura  46209  elaa2lem  46214  etransclem1  46216  etransclem8  46223  etransclem20  46235  etransclem33  46248  etransclem35  46250  etransclem39  46254  rrxtopnfi  46268  ioorrnopnxrlem  46287  sge0tsms  46361  sge0snmpt  46364  sge0fsummpt  46371  sge0pr  46375  sge0lessmpt  46380  sge0iunmptlemfi  46394  sge0iunmptlemre  46396  sge0iunmpt  46399  sge0rpcpnf  46402  sge0isum  46408  nnfoctbdjlem  46436  psmeasure  46452  voliunsge0lem  46453  meaiuninclem  46461  meaiuninc3v  46465  meaiininclem  46467  omeiunltfirp  46500  carageniuncllem2  46503  caratheodorylem1  46507  caratheodorylem2  46508  isomenndlem  46511  hoicvr  46529  hoicvrrex  46537  ovnsupge0  46538  ovnlecvr  46539  ovnf  46544  ovn0lem  46546  ovnsubaddlem1  46551  ovnsubadd  46553  hsphoif  46557  sge0hsphoire  46570  hoidmv1lelem1  46572  hoidmv1lelem2  46573  hoidmv1lelem3  46574  hoidmv1le  46575  hoidmvlelem2  46577  hoidmvlelem3  46578  ovnhoilem1  46582  ovnsubadd2lem  46626  ovolval4lem1  46630  ovolval4lem2  46631  ovolval5lem2  46634  ovnovollem1  46637  ovnovollem2  46638  vonioolem2  46662  vonicclem2  46665  smflim  46758  nsssmfmbflem  46759  smfmullem4  46775  smfsuplem1  46792  smfsuplem3  46794  smflimsuplem3  46803  fsetsnf  47035  cfsetsnfsetf  47042  cfsetsnfsetfo  47044  imasetpreimafvbijlemf  47385  prproropf1o  47491  fmtnodvds  47528  upgrimwlklem2  47882  isubgr3stgrlem6  47955  lincvalsc0  48406  lcoc0  48407  linc0scn0  48408  linc1  48410  lincscm  48415  lincresunit3  48466  1arympt1  48623  1arymaptf  48626  2arympt  48634  2arymaptf  48637  ackendofnn0  48669  amgmlemALT  49788