Theorem fmptd 7061

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052   ↦ cmpt 5167  ⟶wf 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-fun 6495  df-fn 6496  df-f 6497

This theorem is referenced by:  fmpttd  7062  fnwelem  8075  fsetfcdm  8801  fdiagfn  8832  resixpfo  8878  xpmapenlem  9076  unxpdomlem3  9162  fsuppmptdm  9283  cantnfp1lem1  9593  cantnfp1lem2  9594  cantnfp1lem3  9595  cantnf  9608  updjudhf  9849  fseqenlem2  9941  dfac8clem  9948  coftr  10189  isf34lem2  10289  axcc2lem  10352  axdc2lem  10364  axdc3lem4  10369  pwcfsdom  10500  rpnnen1lem1  12922  tpf  14455  caucvg  15635  sumrblem  15667  summolem2a  15671  supcvg  15815  prodrblem  15888  prodmolem2a  15893  crth  16742  eulerthlem1  16745  prmreclem6  16886  4sqlem11  16920  vdwlem2  16947  vdwlem4  16949  vdwlem6  16951  vdwlem10  16955  ramub1lem2  16992  prmgaplcm  17025  frmdup1  18826  grpinvf  18956  mulgnngsum  19049  cycsubm  19171  cycsubgcl  19175  cycsubgss  19176  conjghm  19218  conjnmz  19221  qusghm  19224  galactghm  19373  symgextf  19386  symgfixf  19405  pmtrdifwrdellem1  19450  odf1  19531  dfod2  19533  pgpssslw  19583  frgpmhm  19734  gsummptfidmsplitres  19900  gsummptfidminv  19916  gsumzunsnd  19925  gsummpt1n0  19934  ablfac1b  20041  ablfac2  20060  c0mgm  20433  c0mhm  20434  c0snmgmhm  20436  abvtrivd  20803  issrngd  20826  pwssplit0  21048  rngqiprngimf  21290  mulgghm2  21469  frobrhm  21568  isphld  21647  pjff  21705  frlmup1  21791  asclf  21874  psr1cl  21952  evlslem1  22073  evlsval2  22078  evlsval3  22080  evls1maprhm  22354  rhmmpl  22361  scmatf  22507  mdetf  22573  maduf  22619  pmatcollpw3fi1lem1  22764  chfacfisf  22832  chfacfisfcpmat  22833  cpmidpmatlem2  22849  lly1stc  23474  txcnmpt  23602  txlm  23626  xkoinjcn  23665  kqffn  23703  txflf  23984  tsmsfbas  24106  ustuqtop0  24218  metdsf  24827  metdsge  24828  mulc1cncf  24885  lebnumlem1  24941  cmetcaulem  25268  ovollb2lem  25468  ovolctb  25470  ovolunlem1a  25476  ovolunlem1  25477  ovoliunlem1  25482  ovoliunlem2  25483  ovoliun  25485  ovolshftlem1  25489  ovolscalem1  25493  ovolicc1  25496  ioombl1lem1  25538  uniioombllem2  25563  volsup2  25585  volcn  25586  vitalilem4  25591  vitalilem5  25592  mbfconst  25613  mbfmax  25629  mbfsup  25644  i1f1lem  25669  i1f1  25670  i1fres  25685  itg1climres  25694  itg2splitlem  25728  itg2split  25729  itg2monolem1  25730  itg2mono  25733  itg2i1fseq  25735  itg2i1fseq2  25736  dvreslem  25889  dvmptresicc  25896  dvivthlem1  25988  dvfsumrlimf  26005  dvfsumlem3  26008  ftc1lem2  26016  ftc1lem6  26021  radcnvlem1  26394  pserulm  26403  psercn2  26404  abelthlem4  26415  efif1olem4  26525  lgamgulmlem6  27014  gamcvg  27036  basellem4  27064  basellem7  27067  basellem9  27069  lgsfcl2  27283  lgsqrlem2  27327  lgseisenlem1  27355  dchrmusum2  27474  dchrvmasumiflem1  27481  dchrisum0ff  27487  dchrisum0lem1b  27495  dchrisum0lem2a  27497  abvcxp  27595  padicabv  27610  axlowdimlem15  29042  crctcshwlkn0  29907  wlkiswwlks2lem5  29959  wlkswwlksf1o  29965  wwlksnextfun  29984  clwlkclwwlklem2a  30086  clwlkclwwlkf  30096  clwwlkf  30135  frgrncvvdeqlem4  30390  numclwwlk1lem2f  30443  numclwlk2lem2f  30465  ipblnfi  30944  ubthlem1  30959  htthlem  31006  hlimadd  31282  chscllem1  31726  cnlnadjlem2  32157  strlem3a  32341  hstrlem3a  32349  xppreima2  32742  suppovss  32772  fsuppcurry1  32815  fsuppcurry2  32816  pwrssmgc  33078  mndlactf1  33104  mndlactfo  33105  mndractf1  33106  mndractfo  33107  lmodvslmhm  33129  conjga  33249  rlocf1  33352  nsgmgc  33490  elrspunidl  33506  r1plmhm  33688  r1pquslmic  33689  mplvrpmga  33707  mplvrpmmhm  33708  mplvrpmrhm  33709  psrmonprod  33714  mplmonprod  33716  ply1degltdimlem  33785  ply1degltdim  33786  extdgfialglem1  33855  algextdeglem8  33887  rhmpreimacnlem  34047  rhmpreimacn  34048  xrge0mulc1cn  34104  esumpcvgval  34241  esumcvg  34249  mbfmco2  34428  eulerpartlems  34523  erdszelem9  35400  cvmlift3lem3  35522  ex-sategoelel  35622  ex-sategoelelomsuc  35627  elmrsubrn  35721  mvhf  35759  iprodefisum  35942  unbdqndv1  36787  knoppf  36814  ftc1anclem3  38033  ftc1anclem5  38035  lflnegcl  39538  lshpkrcl  39579  tendo0cl  41253  primrootscoprf  42557  aks6d1c2p1  42574  aks6d1c4  42580  aks6d1c2lem4  42583  aks6d1c2  42586  aks6d1c5lem0  42591  aks6d1c5  42595  sticksstones2  42603  sticksstones8  42609  sticksstones9  42610  sticksstones10  42611  sticksstones11  42612  sticksstones12a  42613  sticksstones17  42619  sticksstones18  42620  aks6d1c6lem2  42627  aks6d1c6lem3  42628  aks6d1c6lem4  42629  aks6d1c6isolem1  42630  aks6d1c6isolem2  42631  aks6d1c6isolem3  42632  aks6d1c6lem5  42633  aks5lem2  42643  frlmsnic  43002  rhmpsr  43012  mplmapghm  43014  evlsbagval  43019  evlsmaprhm  43023  selvcllem5  43032  cantnfub  43770  binomcxplemradcnv  44800  binomcxplemcvg  44802  binomcxplemnotnn0  44804  projf1o  45647  mullimc  46067  ellimcabssub0  46068  mullimcf  46074  constlimc  46075  idlimc  46077  neglimc  46096  addlimc  46097  0ellimcdiv  46098  fnlimf  46127  liminfpnfuz  46265  xlimpnfxnegmnf2  46307  cncfshift  46323  icccncfext  46336  cncfiooiccre  46344  fprodsubrecnncnvlem  46356  fprodaddrecnncnvlem  46358  ioodvbdlimc1lem1  46380  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnxpaek  46391  dvnprodlem1  46395  itgsinexplem1  46403  itgiccshift  46429  dirkercncflem2  46553  fourierdlem4  46560  fourierdlem5  46561  fourierdlem9  46565  fourierdlem14  46570  fourierdlem16  46572  fourierdlem17  46573  fourierdlem18  46574  fourierdlem21  46577  fourierdlem22  46578  fourierdlem37  46593  fourierdlem50  46605  fourierdlem51  46606  fourierdlem53  46608  fourierdlem55  46610  fourierdlem57  46612  fourierdlem58  46613  fourierdlem59  46614  fourierdlem60  46615  fourierdlem61  46616  fourierdlem67  46622  fourierdlem68  46623  fourierdlem72  46627  fourierdlem73  46628  fourierdlem74  46629  fourierdlem75  46630  fourierdlem76  46631  fourierdlem78  46633  fourierdlem80  46635  fourierdlem81  46636  fourierdlem83  46638  fourierdlem84  46639  fourierdlem88  46643  fourierdlem92  46647  fourierdlem93  46648  fourierdlem97  46652  fourierdlem101  46656  fourierdlem103  46658  fourierdlem104  46659  fourierdlem111  46666  sqwvfoura  46677  elaa2lem  46682  etransclem1  46684  etransclem8  46691  etransclem20  46703  etransclem33  46716  etransclem35  46718  etransclem39  46722  rrxtopnfi  46736  ioorrnopnxrlem  46755  sge0tsms  46829  sge0snmpt  46832  sge0fsummpt  46839  sge0pr  46843  sge0lessmpt  46848  sge0iunmptlemfi  46862  sge0iunmptlemre  46864  sge0iunmpt  46867  sge0rpcpnf  46870  sge0isum  46876  nnfoctbdjlem  46904  psmeasure  46920  voliunsge0lem  46921  meaiuninclem  46929  meaiuninc3v  46933  meaiininclem  46935  omeiunltfirp  46968  carageniuncllem2  46971  caratheodorylem1  46975  caratheodorylem2  46976  isomenndlem  46979  hoicvrrex  47005  ovnsupge0  47006  ovnlecvr  47007  ovnf  47012  ovn0lem  47014  ovnsubaddlem1  47019  ovnsubadd  47021  hsphoif  47025  sge0hsphoire  47038  hoidmv1lelem1  47040  hoidmv1lelem2  47041  hoidmv1lelem3  47042  hoidmv1le  47043  hoidmvlelem2  47045  hoidmvlelem3  47046  ovnhoilem1  47050  ovnsubadd2lem  47094  ovolval4lem1  47098  ovolval4lem2  47099  ovolval5lem2  47102  ovnovollem1  47105  ovnovollem2  47106  vonioolem2  47130  vonicclem2  47133  smflim  47226  nsssmfmbflem  47227  smfmullem4  47243  smfsuplem1  47260  smfsuplem3  47262  smflimsuplem3  47271  fsetsnf  47514  cfsetsnfsetf  47521  cfsetsnfsetfo  47523  imasetpreimafvbijlemf  47876  prproropf1o  47982  fmtnodvds  48022  upgrimwlklem2  48389  isubgr3stgrlem6  48462  lincvalsc0  48912  lcoc0  48913  linc0scn0  48914  linc1  48916  lincscm  48921  lincresunit3  48972  1arympt1  49129  1arymaptf  49132  2arympt  49140  2arymaptf  49143  ackendofnn0  49175  amgmlemALT  50293