Theorem fmptd 7134

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∀wral 3059   ↦ cmpt 5231  ⟶wf 6559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-fun 6565  df-fn 6566  df-f 6567

This theorem is referenced by:  fmpttd  7135  fnwelem  8155  fsetfcdm  8899  fdiagfn  8929  resixpfo  8975  xpmapenlem  9183  unxpdomlem3  9286  fsuppmptdm  9414  cantnfp1lem1  9716  cantnfp1lem2  9717  cantnfp1lem3  9718  cantnf  9731  updjudhf  9969  fseqenlem2  10063  dfac8clem  10070  coftr  10311  isf34lem2  10411  axcc2lem  10474  axdc2lem  10486  axdc3lem4  10491  pwcfsdom  10621  rpnnen1lem1  13018  tpf  14535  caucvg  15712  sumrblem  15744  summolem2a  15748  supcvg  15889  prodrblem  15962  prodmolem2a  15967  crth  16812  eulerthlem1  16815  prmreclem6  16955  4sqlem11  16989  vdwlem2  17016  vdwlem4  17018  vdwlem6  17020  vdwlem10  17024  ramub1lem2  17061  prmgaplcm  17094  frmdup1  18890  grpinvf  19017  mulgnngsum  19110  cycsubm  19233  cycsubgcl  19237  cycsubgss  19238  conjghm  19280  conjnmz  19283  qusghm  19286  galactghm  19437  symgextf  19450  symgfixf  19469  pmtrdifwrdellem1  19514  odf1  19595  dfod2  19597  pgpssslw  19647  frgpmhm  19798  gsummptfidmsplitres  19964  gsummptfidminv  19980  gsumzunsnd  19989  gsummpt1n0  19998  ablfac1b  20105  ablfac2  20124  c0mgm  20476  c0mhm  20477  c0snmgmhm  20479  abvtrivd  20850  issrngd  20873  pwssplit0  21075  rngqiprngimf  21325  mulgghm2  21505  frobrhm  21612  isphld  21690  pjff  21750  frlmup1  21836  asclf  21920  psr1cl  21999  evlslem1  22124  evlsval2  22129  evls1maprhm  22396  rhmmpl  22403  scmatf  22551  mdetf  22617  maduf  22663  pmatcollpw3fi1lem1  22808  chfacfisf  22876  chfacfisfcpmat  22877  cpmidpmatlem2  22893  lly1stc  23520  txcnmpt  23648  txlm  23672  xkoinjcn  23711  kqffn  23749  txflf  24030  tsmsfbas  24152  ustuqtop0  24265  metdsf  24884  metdsge  24885  mulc1cncf  24945  lebnumlem1  25007  cmetcaulem  25336  ovollb2lem  25537  ovolctb  25539  ovolunlem1a  25545  ovolunlem1  25546  ovoliunlem1  25551  ovoliunlem2  25552  ovoliun  25554  ovolshftlem1  25558  ovolscalem1  25562  ovolicc1  25565  ioombl1lem1  25607  uniioombllem2  25632  volsup2  25654  volcn  25655  vitalilem4  25660  vitalilem5  25661  mbfconst  25682  mbfmax  25698  mbfsup  25713  i1f1lem  25738  i1f1  25739  i1fres  25755  itg1climres  25764  itg2splitlem  25798  itg2split  25799  itg2monolem1  25800  itg2mono  25803  itg2i1fseq  25805  itg2i1fseq2  25806  dvreslem  25959  dvmptresicc  25966  dvivthlem1  26062  dvfsumrlimf  26080  dvfsumlem3  26084  ftc1lem2  26092  ftc1lem6  26097  radcnvlem1  26471  pserulm  26480  psercn2  26481  psercn2OLD  26482  abelthlem4  26493  efif1olem4  26602  lgamgulmlem6  27092  gamcvg  27114  basellem4  27142  basellem7  27145  basellem9  27147  lgsfcl2  27362  lgsqrlem2  27406  lgseisenlem1  27434  dchrmusum2  27553  dchrvmasumiflem1  27560  dchrisum0ff  27566  dchrisum0lem1b  27574  dchrisum0lem2a  27576  abvcxp  27674  padicabv  27689  axlowdimlem15  28986  crctcshwlkn0  29851  wlkiswwlks2lem5  29903  wlkswwlksf1o  29909  wwlksnextfun  29928  clwlkclwwlklem2a  30027  clwlkclwwlkf  30037  clwwlkf  30076  frgrncvvdeqlem4  30331  numclwwlk1lem2f  30384  numclwlk2lem2f  30406  ipblnfi  30884  ubthlem1  30899  htthlem  30946  hlimadd  31222  chscllem1  31666  cnlnadjlem2  32097  strlem3a  32281  hstrlem3a  32289  xppreima2  32668  suppovss  32696  fsuppcurry1  32743  fsuppcurry2  32744  pwrssmgc  32975  mndlactf1  33014  mndlactfo  33015  mndractf1  33016  mndractfo  33017  lmodvslmhm  33036  rlocf1  33260  nsgmgc  33420  elrspunidl  33436  r1plmhm  33610  r1pquslmic  33611  ply1degltdimlem  33650  ply1degltdim  33651  algextdeglem8  33730  rhmpreimacnlem  33845  rhmpreimacn  33846  xrge0mulc1cn  33902  esumpcvgval  34059  esumcvg  34067  mbfmco2  34247  eulerpartlems  34342  erdszelem9  35184  cvmlift3lem3  35306  ex-sategoelel  35406  ex-sategoelelomsuc  35411  elmrsubrn  35505  mvhf  35543  iprodefisum  35721  unbdqndv1  36491  knoppf  36518  ftc1anclem3  37682  ftc1anclem5  37684  lflnegcl  39057  lshpkrcl  39098  tendo0cl  40773  primrootscoprf  42083  aks6d1c2p1  42100  aks6d1c4  42106  aks6d1c2lem4  42109  aks6d1c2  42112  aks6d1c5lem0  42117  aks6d1c5  42121  sticksstones2  42129  sticksstones8  42135  sticksstones9  42136  sticksstones10  42137  sticksstones11  42138  sticksstones12a  42139  sticksstones17  42145  sticksstones18  42146  aks6d1c6lem2  42153  aks6d1c6lem3  42154  aks6d1c6lem4  42155  aks6d1c6isolem1  42156  aks6d1c6isolem2  42157  aks6d1c6isolem3  42158  aks6d1c6lem5  42159  aks5lem2  42169  metakunt1  42187  metakunt2  42188  metakunt19  42205  metakunt25  42211  frlmsnic  42527  rhmpsr  42539  mplmapghm  42543  evlsval3  42546  evlsbagval  42553  evlsmaprhm  42557  selvcllem5  42569  cantnfub  43311  binomcxplemradcnv  44348  binomcxplemcvg  44350  binomcxplemnotnn0  44352  projf1o  45140  mullimc  45572  ellimcabssub0  45573  mullimcf  45579  constlimc  45580  idlimc  45582  neglimc  45603  addlimc  45604  0ellimcdiv  45605  fnlimf  45634  liminfpnfuz  45772  xlimpnfxnegmnf2  45814  cncfshift  45830  icccncfext  45843  cncfiooiccre  45851  fprodsubrecnncnvlem  45863  fprodaddrecnncnvlem  45865  ioodvbdlimc1lem1  45887  ioodvbdlimc1lem2  45888  ioodvbdlimc2lem  45890  dvnxpaek  45898  dvnprodlem1  45902  itgsinexplem1  45910  itgiccshift  45936  dirkercncflem2  46060  fourierdlem4  46067  fourierdlem5  46068  fourierdlem9  46072  fourierdlem14  46077  fourierdlem16  46079  fourierdlem17  46080  fourierdlem18  46081  fourierdlem21  46084  fourierdlem22  46085  fourierdlem37  46100  fourierdlem50  46112  fourierdlem51  46113  fourierdlem53  46115  fourierdlem55  46117  fourierdlem57  46119  fourierdlem58  46120  fourierdlem59  46121  fourierdlem60  46122  fourierdlem61  46123  fourierdlem67  46129  fourierdlem68  46130  fourierdlem72  46134  fourierdlem73  46135  fourierdlem74  46136  fourierdlem75  46137  fourierdlem76  46138  fourierdlem78  46140  fourierdlem80  46142  fourierdlem81  46143  fourierdlem83  46145  fourierdlem84  46146  fourierdlem88  46150  fourierdlem92  46154  fourierdlem93  46155  fourierdlem97  46159  fourierdlem101  46163  fourierdlem103  46165  fourierdlem104  46166  fourierdlem111  46173  sqwvfoura  46184  elaa2lem  46189  etransclem1  46191  etransclem8  46198  etransclem20  46210  etransclem33  46223  etransclem35  46225  etransclem39  46229  rrxtopnfi  46243  ioorrnopnxrlem  46262  sge0tsms  46336  sge0snmpt  46339  sge0fsummpt  46346  sge0pr  46350  sge0lessmpt  46355  sge0iunmptlemfi  46369  sge0iunmptlemre  46371  sge0iunmpt  46374  sge0rpcpnf  46377  sge0isum  46383  nnfoctbdjlem  46411  psmeasure  46427  voliunsge0lem  46428  meaiuninclem  46436  meaiuninc3v  46440  meaiininclem  46442  omeiunltfirp  46475  carageniuncllem2  46478  caratheodorylem1  46482  caratheodorylem2  46483  isomenndlem  46486  hoicvr  46504  hoicvrrex  46512  ovnsupge0  46513  ovnlecvr  46514  ovnf  46519  ovn0lem  46521  ovnsubaddlem1  46526  ovnsubadd  46528  hsphoif  46532  sge0hsphoire  46545  hoidmv1lelem1  46547  hoidmv1lelem2  46548  hoidmv1lelem3  46549  hoidmv1le  46550  hoidmvlelem2  46552  hoidmvlelem3  46553  ovnhoilem1  46557  ovnsubadd2lem  46601  ovolval4lem1  46605  ovolval4lem2  46606  ovolval5lem2  46609  ovnovollem1  46612  ovnovollem2  46613  vonioolem2  46637  vonicclem2  46640  smflim  46733  nsssmfmbflem  46734  smfmullem4  46750  smfsuplem1  46767  smfsuplem3  46769  smflimsuplem3  46778  fsetsnf  47001  cfsetsnfsetf  47008  cfsetsnfsetfo  47010  imasetpreimafvbijlemf  47326  prproropf1o  47432  fmtnodvds  47469  isubgr3stgrlem6  47874  lincvalsc0  48267  lcoc0  48268  linc0scn0  48269  linc1  48271  lincscm  48276  lincresunit3  48327  1arympt1  48488  1arymaptf  48491  2arympt  48499  2arymaptf  48502  ackendofnn0  48534  amgmlemALT  49034