Theorem fmptd 6997

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107  ∀wral 3065   ↦ cmpt 5158  ⟶wf 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-fun 6439  df-fn 6440  df-f 6441

This theorem is referenced by:  fmpttd  6998  rnmptcOLD  7092  fnwelem  7981  fsetfcdm  8657  fsetfocdm  8658  fdiagfn  8687  resixpfo  8733  xpmapenlem  8940  unxpdomlem3  9038  fsuppmptdm  9148  cantnfp1lem1  9445  cantnfp1lem2  9446  cantnfp1lem3  9447  cantnf  9460  updjudhf  9698  fseqenlem2  9790  dfac8clem  9797  coftr  10038  isf34lem2  10138  axcc2lem  10201  axdc2lem  10213  axdc3lem4  10218  pwcfsdom  10348  rpnnen1lem1  12727  caucvg  15399  sumrblem  15432  summolem2a  15436  supcvg  15577  prodrblem  15648  prodmolem2a  15653  crth  16488  eulerthlem1  16491  prmreclem6  16631  4sqlem11  16665  vdwlem2  16692  vdwlem4  16694  vdwlem6  16696  vdwlem10  16700  ramub1lem2  16737  prmgaplcm  16770  frmdup1  18512  grpinvf  18635  mulgnngsum  18718  cycsubm  18830  cycsubgcl  18834  cycsubgss  18835  conjghm  18874  conjnmz  18877  qusghm  18880  galactghm  19021  symgextf  19034  symgfixf  19053  pmtrdifwrdellem1  19098  odf1  19178  dfod2  19180  pgpssslw  19228  frgpmhm  19380  gsummptfidmsplitres  19541  gsummptfidminv  19557  gsumzunsnd  19566  gsummpt1n0  19575  ablfac1b  19682  ablfac2  19701  abvtrivd  20109  issrngd  20130  pwssplit0  20329  mulgghm2  20707  isphld  20868  pjff  20928  frlmup1  21014  asclf  21095  psr1cl  21180  evlslem1  21301  evlsval2  21306  scmatf  21687  mdetf  21753  maduf  21799  pmatcollpw3fi1lem1  21944  chfacfisf  22012  chfacfisfcpmat  22013  cpmidpmatlem2  22029  lly1stc  22656  txcnmpt  22784  txlm  22808  xkoinjcn  22847  kqffn  22885  txflf  23166  tsmsfbas  23288  ustuqtop0  23401  metdsf  24020  metdsge  24021  mulc1cncf  24077  lebnumlem1  24133  cmetcaulem  24461  ovollb2lem  24661  ovolctb  24663  ovolunlem1a  24669  ovolunlem1  24670  ovoliunlem1  24675  ovoliunlem2  24676  ovoliun  24678  ovolshftlem1  24682  ovolscalem1  24686  ovolicc1  24689  ioombl1lem1  24731  uniioombllem2  24756  volsup2  24778  volcn  24779  vitalilem4  24784  vitalilem5  24785  mbfconst  24806  mbfmax  24822  mbfsup  24837  i1f1lem  24862  i1f1  24863  i1fres  24879  itg1climres  24888  itg2splitlem  24922  itg2split  24923  itg2monolem1  24924  itg2mono  24927  itg2i1fseq  24929  itg2i1fseq2  24930  dvreslem  25082  dvmptresicc  25089  dvivthlem1  25181  dvfsumrlimf  25198  dvfsumlem3  25201  ftc1lem2  25209  ftc1lem6  25214  tdeglem1OLD  25230  radcnvlem1  25581  pserulm  25590  psercn2  25591  abelthlem4  25602  efif1olem4  25710  lgamgulmlem6  26192  gamcvg  26214  basellem4  26242  basellem7  26245  basellem9  26247  lgsfcl2  26460  lgsqrlem2  26504  lgseisenlem1  26532  dchrmusum2  26651  dchrvmasumiflem1  26658  dchrisum0ff  26664  dchrisum0lem1b  26672  dchrisum0lem2a  26674  abvcxp  26772  padicabv  26787  axlowdimlem15  27333  crctcshwlkn0  28195  wlkiswwlks2lem5  28247  wlkswwlksf1o  28253  wwlksnextfun  28272  clwlkclwwlklem2a  28371  clwlkclwwlkf  28381  clwwlkf  28420  frgrncvvdeqlem4  28675  numclwwlk1lem2f  28728  numclwlk2lem2f  28750  ipblnfi  29226  ubthlem1  29241  htthlem  29288  hlimadd  29564  chscllem1  30008  cnlnadjlem2  30439  strlem3a  30623  hstrlem3a  30631  xppreima2  30997  suppovss  31026  fsuppcurry1  31069  fsuppcurry2  31070  pwrssmgc  31287  lmodvslmhm  31319  frobrhm  31494  nsgmgc  31606  elrspunidl  31615  rhmpreimacnlem  31843  rhmpreimacn  31844  xrge0mulc1cn  31900  esumpcvgval  32055  esumcvg  32063  mbfmco2  32241  eulerpartlems  32336  erdszelem9  33170  cvmlift3lem3  33292  ex-sategoelel  33392  ex-sategoelelomsuc  33397  elmrsubrn  33491  mvhf  33529  iprodefisum  33716  unbdqndv1  34697  knoppf  34724  ftc1anclem3  35861  ftc1anclem5  35863  lflnegcl  37096  lshpkrcl  37137  tendo0cl  38811  sticksstones2  40110  sticksstones8  40116  sticksstones9  40117  sticksstones10  40118  sticksstones11  40119  sticksstones12a  40120  sticksstones17  40126  sticksstones18  40127  metakunt1  40132  metakunt2  40133  metakunt19  40150  metakunt25  40156  selvval2lem5  40236  frlmsnic  40270  evlsval3  40279  evlsbagval  40282  binomcxplemradcnv  41977  binomcxplemcvg  41979  binomcxplemnotnn0  41981  projf1o  42743  mullimc  43164  ellimcabssub0  43165  mullimcf  43171  constlimc  43172  idlimc  43174  neglimc  43195  addlimc  43196  0ellimcdiv  43197  fnlimf  43226  liminfpnfuz  43364  xlimpnfxnegmnf2  43406  cncfshift  43422  icccncfext  43435  cncfiooiccre  43443  fprodsubrecnncnvlem  43455  fprodaddrecnncnvlem  43457  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnxpaek  43490  dvnprodlem1  43494  itgsinexplem1  43502  itgiccshift  43528  dirkercncflem2  43652  fourierdlem4  43659  fourierdlem5  43660  fourierdlem9  43664  fourierdlem14  43669  fourierdlem16  43671  fourierdlem17  43672  fourierdlem18  43673  fourierdlem21  43676  fourierdlem22  43677  fourierdlem37  43692  fourierdlem50  43704  fourierdlem51  43705  fourierdlem53  43707  fourierdlem55  43709  fourierdlem57  43711  fourierdlem58  43712  fourierdlem59  43713  fourierdlem60  43714  fourierdlem61  43715  fourierdlem67  43721  fourierdlem68  43722  fourierdlem72  43726  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem78  43732  fourierdlem80  43734  fourierdlem81  43735  fourierdlem83  43737  fourierdlem84  43738  fourierdlem88  43742  fourierdlem92  43746  fourierdlem93  43747  fourierdlem97  43751  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  sqwvfoura  43776  elaa2lem  43781  etransclem1  43783  etransclem8  43790  etransclem20  43802  etransclem33  43815  etransclem35  43817  etransclem39  43821  rrxtopnfi  43835  ioorrnopnxrlem  43854  sge0tsms  43925  sge0snmpt  43928  sge0fsummpt  43935  sge0pr  43939  sge0lessmpt  43944  sge0iunmptlemfi  43958  sge0iunmptlemre  43960  sge0iunmpt  43963  sge0rpcpnf  43966  sge0isum  43972  nnfoctbdjlem  44000  psmeasure  44016  voliunsge0lem  44017  meaiuninclem  44025  meaiuninc3v  44029  meaiininclem  44031  omeiunltfirp  44064  carageniuncllem2  44067  caratheodorylem1  44071  caratheodorylem2  44072  isomenndlem  44075  hoicvr  44093  hoicvrrex  44101  ovnsupge0  44102  ovnlecvr  44103  ovnf  44108  ovn0lem  44110  ovnsubaddlem1  44115  ovnsubadd  44117  hsphoif  44121  sge0hsphoire  44134  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmv1le  44139  hoidmvlelem2  44141  hoidmvlelem3  44142  ovnhoilem1  44146  ovnsubadd2lem  44190  ovolval4lem1  44194  ovolval4lem2  44195  ovolval5lem2  44198  ovnovollem1  44201  ovnovollem2  44202  vonioolem2  44226  vonicclem2  44229  smflim  44322  nsssmfmbflem  44323  smfmullem4  44339  smfsuplem1  44355  smfsuplem3  44357  smflimsuplem3  44366  fsetsnf  44556  cfsetsnfsetf  44563  cfsetsnfsetfo  44565  imasetpreimafvbijlemf  44864  prproropf1o  44970  fmtnodvds  45007  c0mgm  45478  c0mhm  45479  c0snmgmhm  45483  lincvalsc0  45773  lcoc0  45774  linc0scn0  45775  linc1  45777  lincscm  45782  lincresunit3  45833  1arympt1  45995  1arymaptf  45998  2arympt  46006  2arymaptf  46009  ackendofnn0  46041  amgmlemALT  46518