Theorem fmptd 7047

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∀wral 3047   ↦ cmpt 5170  ⟶wf 6477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-fun 6483  df-fn 6484  df-f 6485

This theorem is referenced by:  fmpttd  7048  fnwelem  8061  fsetfcdm  8784  fdiagfn  8814  resixpfo  8860  xpmapenlem  9057  unxpdomlem3  9142  fsuppmptdm  9260  cantnfp1lem1  9568  cantnfp1lem2  9569  cantnfp1lem3  9570  cantnf  9583  updjudhf  9824  fseqenlem2  9916  dfac8clem  9923  coftr  10164  isf34lem2  10264  axcc2lem  10327  axdc2lem  10339  axdc3lem4  10344  pwcfsdom  10474  rpnnen1lem1  12876  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  18772  grpinvf  18899  mulgnngsum  18992  cycsubm  19114  cycsubgcl  19118  cycsubgss  19119  conjghm  19161  conjnmz  19164  qusghm  19167  galactghm  19316  symgextf  19329  symgfixf  19348  pmtrdifwrdellem1  19393  odf1  19474  dfod2  19476  pgpssslw  19526  frgpmhm  19677  gsummptfidmsplitres  19843  gsummptfidminv  19859  gsumzunsnd  19868  gsummpt1n0  19877  ablfac1b  19984  ablfac2  20003  c0mgm  20377  c0mhm  20378  c0snmgmhm  20380  abvtrivd  20747  issrngd  20770  pwssplit0  20992  rngqiprngimf  21234  mulgghm2  21413  frobrhm  21512  isphld  21591  pjff  21649  frlmup1  21735  asclf  21819  psr1cl  21898  evlslem1  22017  evlsval2  22022  evls1maprhm  22291  rhmmpl  22298  scmatf  22444  mdetf  22510  maduf  22556  pmatcollpw3fi1lem1  22701  chfacfisf  22769  chfacfisfcpmat  22770  cpmidpmatlem2  22786  lly1stc  23411  txcnmpt  23539  txlm  23563  xkoinjcn  23602  kqffn  23640  txflf  23921  tsmsfbas  24043  ustuqtop0  24155  metdsf  24764  metdsge  24765  mulc1cncf  24825  lebnumlem1  24887  cmetcaulem  25215  ovollb2lem  25416  ovolctb  25418  ovolunlem1a  25424  ovolunlem1  25425  ovoliunlem1  25430  ovoliunlem2  25431  ovoliun  25433  ovolshftlem1  25437  ovolscalem1  25441  ovolicc1  25444  ioombl1lem1  25486  uniioombllem2  25511  volsup2  25533  volcn  25534  vitalilem4  25539  vitalilem5  25540  mbfconst  25561  mbfmax  25577  mbfsup  25592  i1f1lem  25617  i1f1  25618  i1fres  25633  itg1climres  25642  itg2splitlem  25676  itg2split  25677  itg2monolem1  25678  itg2mono  25681  itg2i1fseq  25683  itg2i1fseq2  25684  dvreslem  25837  dvmptresicc  25844  dvivthlem1  25940  dvfsumrlimf  25958  dvfsumlem3  25962  ftc1lem2  25970  ftc1lem6  25975  radcnvlem1  26349  pserulm  26358  psercn2  26359  psercn2OLD  26360  abelthlem4  26371  efif1olem4  26481  lgamgulmlem6  26971  gamcvg  26993  basellem4  27021  basellem7  27024  basellem9  27026  lgsfcl2  27241  lgsqrlem2  27285  lgseisenlem1  27313  dchrmusum2  27432  dchrvmasumiflem1  27439  dchrisum0ff  27445  dchrisum0lem1b  27453  dchrisum0lem2a  27455  abvcxp  27553  padicabv  27568  axlowdimlem15  28934  crctcshwlkn0  29799  wlkiswwlks2lem5  29851  wlkswwlksf1o  29857  wwlksnextfun  29876  clwlkclwwlklem2a  29978  clwlkclwwlkf  29988  clwwlkf  30027  frgrncvvdeqlem4  30282  numclwwlk1lem2f  30335  numclwlk2lem2f  30357  ipblnfi  30835  ubthlem1  30850  htthlem  30897  hlimadd  31173  chscllem1  31617  cnlnadjlem2  32048  strlem3a  32232  hstrlem3a  32240  xppreima2  32633  suppovss  32662  fsuppcurry1  32707  fsuppcurry2  32708  pwrssmgc  32981  mndlactf1  33007  mndlactfo  33008  mndractf1  33009  mndractfo  33010  lmodvslmhm  33030  conjga  33139  rlocf1  33240  nsgmgc  33377  elrspunidl  33393  r1plmhm  33570  r1pquslmic  33571  mplvrpmga  33575  mplvrpmmhm  33576  mplvrpmrhm  33577  ply1degltdimlem  33635  ply1degltdim  33636  extdgfialglem1  33705  algextdeglem8  33737  rhmpreimacnlem  33897  rhmpreimacn  33898  xrge0mulc1cn  33954  esumpcvgval  34091  esumcvg  34099  mbfmco2  34278  eulerpartlems  34373  erdszelem9  35243  cvmlift3lem3  35365  ex-sategoelel  35465  ex-sategoelelomsuc  35470  elmrsubrn  35564  mvhf  35602  iprodefisum  35785  unbdqndv1  36550  knoppf  36577  ftc1anclem3  37743  ftc1anclem5  37745  lflnegcl  39122  lshpkrcl  39163  tendo0cl  40837  primrootscoprf  42142  aks6d1c2p1  42159  aks6d1c4  42165  aks6d1c2lem4  42168  aks6d1c2  42171  aks6d1c5lem0  42176  aks6d1c5  42180  sticksstones2  42188  sticksstones8  42194  sticksstones9  42195  sticksstones10  42196  sticksstones11  42197  sticksstones12a  42198  sticksstones17  42204  sticksstones18  42205  aks6d1c6lem2  42212  aks6d1c6lem3  42213  aks6d1c6lem4  42214  aks6d1c6isolem1  42215  aks6d1c6isolem2  42216  aks6d1c6isolem3  42217  aks6d1c6lem5  42218  aks5lem2  42228  frlmsnic  42581  rhmpsr  42593  mplmapghm  42597  evlsval3  42600  evlsbagval  42607  evlsmaprhm  42611  selvcllem5  42623  cantnfub  43362  binomcxplemradcnv  44393  binomcxplemcvg  44395  binomcxplemnotnn0  44397  projf1o  45242  mullimc  45664  ellimcabssub0  45665  mullimcf  45671  constlimc  45672  idlimc  45674  neglimc  45693  addlimc  45694  0ellimcdiv  45695  fnlimf  45724  liminfpnfuz  45862  xlimpnfxnegmnf2  45904  cncfshift  45920  icccncfext  45933  cncfiooiccre  45941  fprodsubrecnncnvlem  45953  fprodaddrecnncnvlem  45955  ioodvbdlimc1lem1  45977  ioodvbdlimc1lem2  45978  ioodvbdlimc2lem  45980  dvnxpaek  45988  dvnprodlem1  45992  itgsinexplem1  46000  itgiccshift  46026  dirkercncflem2  46150  fourierdlem4  46157  fourierdlem5  46158  fourierdlem9  46162  fourierdlem14  46167  fourierdlem16  46169  fourierdlem17  46170  fourierdlem18  46171  fourierdlem21  46174  fourierdlem22  46175  fourierdlem37  46190  fourierdlem50  46202  fourierdlem51  46203  fourierdlem53  46205  fourierdlem55  46207  fourierdlem57  46209  fourierdlem58  46210  fourierdlem59  46211  fourierdlem60  46212  fourierdlem61  46213  fourierdlem67  46219  fourierdlem68  46220  fourierdlem72  46224  fourierdlem73  46225  fourierdlem74  46226  fourierdlem75  46227  fourierdlem76  46228  fourierdlem78  46230  fourierdlem80  46232  fourierdlem81  46233  fourierdlem83  46235  fourierdlem84  46236  fourierdlem88  46240  fourierdlem92  46244  fourierdlem93  46245  fourierdlem97  46249  fourierdlem101  46253  fourierdlem103  46255  fourierdlem104  46256  fourierdlem111  46263  sqwvfoura  46274  elaa2lem  46279  etransclem1  46281  etransclem8  46288  etransclem20  46300  etransclem33  46313  etransclem35  46315  etransclem39  46319  rrxtopnfi  46333  ioorrnopnxrlem  46352  sge0tsms  46426  sge0snmpt  46429  sge0fsummpt  46436  sge0pr  46440  sge0lessmpt  46445  sge0iunmptlemfi  46459  sge0iunmptlemre  46461  sge0iunmpt  46464  sge0rpcpnf  46467  sge0isum  46473  nnfoctbdjlem  46501  psmeasure  46517  voliunsge0lem  46518  meaiuninclem  46526  meaiuninc3v  46530  meaiininclem  46532  omeiunltfirp  46565  carageniuncllem2  46568  caratheodorylem1  46572  caratheodorylem2  46573  isomenndlem  46576  hoicvr  46594  hoicvrrex  46602  ovnsupge0  46603  ovnlecvr  46604  ovnf  46609  ovn0lem  46611  ovnsubaddlem1  46616  ovnsubadd  46618  hsphoif  46622  sge0hsphoire  46635  hoidmv1lelem1  46637  hoidmv1lelem2  46638  hoidmv1lelem3  46639  hoidmv1le  46640  hoidmvlelem2  46642  hoidmvlelem3  46643  ovnhoilem1  46647  ovnsubadd2lem  46691  ovolval4lem1  46695  ovolval4lem2  46696  ovolval5lem2  46699  ovnovollem1  46702  ovnovollem2  46703  vonioolem2  46727  vonicclem2  46730  smflim  46823  nsssmfmbflem  46824  smfmullem4  46840  smfsuplem1  46857  smfsuplem3  46859  smflimsuplem3  46868  fsetsnf  47090  cfsetsnfsetf  47097  cfsetsnfsetfo  47099  imasetpreimafvbijlemf  47440  prproropf1o  47546  fmtnodvds  47583  upgrimwlklem2  47937  isubgr3stgrlem6  48010  lincvalsc0  48461  lcoc0  48462  linc0scn0  48463  linc1  48465  lincscm  48470  lincresunit3  48521  1arympt1  48678  1arymaptf  48681  2arympt  48689  2arymaptf  48692  ackendofnn0  48724  amgmlemALT  49843