Theorem fmptd 7119

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076   ↦ cmpt 5185  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6545  df-fn 6546  df-f 6547

This theorem is used by:  fmpttd  7120  fnwelem  8150  fsetfcdm  8890  fdiagfn  8926  resixpfo  8972  xpmapenlem  9171  unxpdomlem3  9257  fsuppmptdm  9375  cantnfp1lem1  9686  cantnfp1lem2  9687  cantnfp1lem3  9688  cantnf  9701  updjudhf  10019  fseqenlem2  10111  dfac8clem  10118  coftr  10358  isf34lem2  10458  axcc2lem  10521  axdc2lem  10533  axdc3lem4  10538  pwcfsdom  10675  rpnnen1lem1  13113  tpf  14651  caucvg  15855  sumrblem  15886  summolem2a  15890  supcvg  16034  prodrblem  16105  prodmolem2a  16110  crth  16964  eulerthlem1  16967  prmreclem6  17108  4sqlem11  17142  vdwlem2  17169  vdwlem4  17171  vdwlem6  17173  vdwlem10  17177  ramub1lem2  17214  prmgaplcm  17247  frmdup1  19069  grpinvf  19206  mulgnngsum  19298  cycsubm  19426  cycsubgcl  19430  cycsubgss  19431  conjghm  19472  conjnmz  19475  qusghm  19478  galactghm  19627  symgextf  19640  symgfixf  19659  pmtrdifwrdellem1  19704  odf1  19785  dfod2  19787  pgpssslw  19837  frgpmhm  19988  gsummptfidmsplitres  20154  gsummptfidminv  20170  gsumzunsnd  20179  gsummpt1n0  20188  ablfac1b  20295  ablfac2  20314  c0mgm  20698  c0mhm  20699  c0snmgmhm  20701  abvtrivd  21098  issrngd  21121  pwssplit0  21342  rngqiprngimf  21602  mulgghm2  21791  frobrhm  21890  isphld  21969  pjff  22027  frlmup1  22113  asclf  22198  psr1cl  22277  evlslem1  22400  evlsval2  22405  evlsval3  22407  mplmapghm  22440  evlsmaprhm  22449  selvcllem5  22457  evls1maprhm  22703  rhmmpl  22707  scmatf  22853  mdetf  22919  maduf  22965  pmatcollpw3fi1lem1  23113  chfacfisf  23181  chfacfisfcpmat  23182  cpmidpmatlem2  23198  lly1stc  23824  txcnmpt  23952  txlm  23976  xkoinjcn  24015  kqffn  24053  txflf  24334  tsmsfbas  24456  ustuqtop0  24568  metdsf  25177  metdsge  25178  mulc1cncf  25235  lebnumlem1  25291  cmetcaulem  25618  ovollb2lem  25818  ovolctb  25820  ovolunlem1a  25826  ovolunlem1  25827  ovoliunlem1  25832  ovoliunlem2  25833  ovoliun  25835  ovolshftlem1  25839  ovolscalem1  25843  ovolicc1  25846  ioombl1lem1  25888  uniioombllem2  25913  volsup2  25935  volcn  25936  vitalilem4  25941  vitalilem5  25942  mbfconst  25963  mbfmax  25979  mbfsup  25994  i1f1lem  26019  i1f1  26020  i1fres  26035  itg1climres  26044  itg2splitlem  26078  itg2split  26079  itg2monolem1  26080  itg2mono  26083  itg2i1fseq  26085  itg2i1fseq2  26086  dvreslem  26238  dvmptresicc  26245  dvivthlem1  26337  dvfsumrlimf  26354  dvfsumlem3  26357  ftc1lem2  26365  ftc1lem6  26370  radcnvlem1  26749  pserulm  26758  psercn2  26759  abelthlem4  26770  efif1olem4  26882  lgamgulmlem6  27370  gamcvg  27392  basellem4  27420  basellem7  27423  basellem9  27425  lgsfcl2  27639  lgsqrlem2  27683  lgseisenlem1  27711  dchrmusum2  27830  dchrvmasumiflem1  27837  dchrisum0ff  27843  dchrisum0lem1b  27851  dchrisum0lem2a  27853  abvcxp  27951  padicabv  27966  axlowdimlem15  29543  crctcshwlkn0  30419  wlkiswwlks2lem5  30471  wlkswwlksf1o  30477  wwlksnextfun  30496  clwlkclwwlklem2a  30598  clwlkclwwlkf  30608  clwwlkf  30647  frgrncvvdeqlem4  30912  numclwwlk1lem2f  30965  numclwlk2lem2f  30987  ipblnfi  31466  ubthlem1  31481  htthlem  31528  hlimadd  31804  chscllem1  32248  cnlnadjlem2  32679  strlem3a  32863  hstrlem3a  32871  xppreima2  33296  suppovss  33325  fsuppcurry1  33366  fsuppcurry2  33367  pwrssmgc  33611  mndlactf1  33637  mndlactfo  33638  mndractf1  33639  mndractfo  33640  lmodvslmhm  33661  conjga  33781  rlocf1  33885  nsgmgc  34013  elrspunidl  34028  r1plmhm  34191  r1pquslmic  34192  selvply1rhmlem1  34202  mplvrpmga  34227  mplvrpmmhm  34228  mplvrpmrhm  34229  psrmonprod  34234  mplmonprod  34236  ply1degltdimlem  34304  ply1degltdim  34305  extdgfialglem1  34374  algextdeglem8  34406  rhmpreimacnlem  34566  rhmpreimacn  34567  xrge0mulc1cn  34623  esumpcvgval  34760  esumcvg  34768  mbfmco2  34947  eulerpartlems  35042  onvfowev  36001  erdszelem9  36082  cvmlift3lem3  36204  ex-sategoelel  36304  ex-sategoelelomsuc  36309  elmrsubrn  36403  mvhf  36441  iprodefisum  36630  unbdqndv1  37498  knoppf  37525  ftc1anclem3  38750  ftc1anclem5  38752  lflnegcl  40269  lshpkrcl  40310  tendo0cl  41984  primrootscoprf  43288  aks6d1c2p1  43305  aks6d1c4  43311  aks6d1c2lem4  43314  aks6d1c2  43317  aks6d1c5lem0  43322  aks6d1c5  43326  sticksstones2  43334  sticksstones8  43340  sticksstones9  43341  sticksstones10  43342  sticksstones11  43343  sticksstones12a  43344  sticksstones17  43350  sticksstones18  43351  aks6d1c6lem2  43358  aks6d1c6lem3  43359  aks6d1c6lem4  43360  aks6d1c6isolem1  43361  aks6d1c6isolem2  43362  aks6d1c6isolem3  43363  aks6d1c6lem5  43364  aks5lem2  43374  frlmsnic  43741  rhmpsr  43748  evlsbagval  43751  cantnfub  44460  binomcxplemradcnv  45473  binomcxplemcvg  45475  binomcxplemnotnn0  45477  projf1o  46347  mullimc  46764  ellimcabssub0  46765  mullimcf  46771  constlimc  46772  idlimc  46774  neglimc  46793  addlimc  46794  0ellimcdiv  46795  fnlimf  46824  liminfpnfuz  46962  xlimpnfxnegmnf2  47004  cncfshift  47020  icccncfext  47033  cncfiooiccre  47041  fprodsubrecnncnvlem  47053  fprodaddrecnncnvlem  47055  ioodvbdlimc1lem1  47077  ioodvbdlimc1lem2  47078  ioodvbdlimc2lem  47080  dvnxpaek  47088  dvnprodlem1  47092  itgsinexplem1  47100  itgiccshift  47126  dirkercncflem2  47250  fourierdlem4  47257  fourierdlem5  47258  fourierdlem9  47262  fourierdlem14  47267  fourierdlem16  47269  fourierdlem17  47270  fourierdlem18  47271  fourierdlem21  47274  fourierdlem22  47275  fourierdlem37  47290  fourierdlem50  47302  fourierdlem51  47303  fourierdlem53  47305  fourierdlem55  47307  fourierdlem57  47309  fourierdlem58  47310  fourierdlem59  47311  fourierdlem60  47312  fourierdlem61  47313  fourierdlem67  47319  fourierdlem68  47320  fourierdlem72  47324  fourierdlem73  47325  fourierdlem74  47326  fourierdlem75  47327  fourierdlem76  47328  fourierdlem78  47330  fourierdlem80  47332  fourierdlem81  47333  fourierdlem83  47335  fourierdlem84  47336  fourierdlem88  47340  fourierdlem92  47344  fourierdlem93  47345  fourierdlem97  47349  fourierdlem101  47353  fourierdlem103  47355  fourierdlem104  47356  fourierdlem111  47363  sqwvfoura  47374  elaa2lem  47379  etransclem1  47381  etransclem8  47388  etransclem20  47400  etransclem33  47413  etransclem35  47415  etransclem39  47419  rrxtopnfi  47433  ioorrnopnxrlem  47452  sge0tsms  47526  sge0snmpt  47529  sge0fsummpt  47536  sge0pr  47540  sge0lessmpt  47545  sge0iunmptlemfi  47559  sge0iunmptlemre  47561  sge0iunmpt  47564  sge0rpcpnf  47567  sge0isum  47573  nnfoctbdjlem  47601  psmeasure  47617  voliunsge0lem  47618  meaiuninclem  47626  meaiuninc3v  47630  meaiininclem  47632  omeiunltfirp  47665  carageniuncllem2  47668  caratheodorylem1  47672  caratheodorylem2  47673  isomenndlem  47676  hoicvrrex  47702  ovnsupge0  47703  ovnlecvr  47704  ovnf  47709  ovn0lem  47711  ovnsubaddlem1  47716  ovnsubadd  47718  hsphoif  47722  sge0hsphoire  47735  hoidmv1lelem1  47737  hoidmv1lelem2  47738  hoidmv1lelem3  47739  hoidmv1le  47740  hoidmvlelem2  47742  hoidmvlelem3  47743  ovnhoilem1  47747  ovnsubadd2lem  47791  ovolval4lem1  47795  ovolval4lem2  47796  ovolval5lem2  47799  ovnovollem1  47802  ovnovollem2  47803  vonioolem2  47827  vonicclem2  47830  smflim  47923  nsssmfmbflem  47924  smfmullem4  47940  smfsuplem1  47957  smfsuplem3  47959  smflimsuplem3  47968  fsetsnf  48257  cfsetsnfsetf  48264  cfsetsnfsetfo  48266  imasetpreimafvbijlemf  48619  prproropf1o  48725  fmtnodvds  48765  upgrimwlklem2  49132  isubgr3stgrlem6  49205  lincvalsc0  49669  lcoc0  49670  linc0scn0  49671  linc1  49673  lincscm  49678  lincresunit3  49729  1arympt1  49886  1arymaptf  49889  2arympt  49897  2arymaptf  49900  ackendofnn0  49932  amgmlemALT  51199