Theorem fmptd 7059

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3051   ↦ cmpt 5179  ⟶wf 6488

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  fmpttd  7060  fnwelem  8073  fsetfcdm  8797  fdiagfn  8828  resixpfo  8874  xpmapenlem  9072  unxpdomlem3  9158  fsuppmptdm  9279  cantnfp1lem1  9587  cantnfp1lem2  9588  cantnfp1lem3  9589  cantnf  9602  updjudhf  9843  fseqenlem2  9935  dfac8clem  9942  coftr  10183  isf34lem2  10283  axcc2lem  10346  axdc2lem  10358  axdc3lem4  10363  pwcfsdom  10494  rpnnen1lem1  12891  tpf  14422  caucvg  15602  sumrblem  15634  summolem2a  15638  supcvg  15779  prodrblem  15852  prodmolem2a  15857  crth  16705  eulerthlem1  16708  prmreclem6  16849  4sqlem11  16883  vdwlem2  16910  vdwlem4  16912  vdwlem6  16914  vdwlem10  16918  ramub1lem2  16955  prmgaplcm  16988  frmdup1  18789  grpinvf  18916  mulgnngsum  19009  cycsubm  19131  cycsubgcl  19135  cycsubgss  19136  conjghm  19178  conjnmz  19181  qusghm  19184  galactghm  19333  symgextf  19346  symgfixf  19365  pmtrdifwrdellem1  19410  odf1  19491  dfod2  19493  pgpssslw  19543  frgpmhm  19694  gsummptfidmsplitres  19860  gsummptfidminv  19876  gsumzunsnd  19885  gsummpt1n0  19894  ablfac1b  20001  ablfac2  20020  c0mgm  20395  c0mhm  20396  c0snmgmhm  20398  abvtrivd  20765  issrngd  20788  pwssplit0  21010  rngqiprngimf  21252  mulgghm2  21431  frobrhm  21530  isphld  21609  pjff  21667  frlmup1  21753  asclf  21837  psr1cl  21916  evlslem1  22037  evlsval2  22042  evlsval3  22044  evls1maprhm  22320  rhmmpl  22327  scmatf  22473  mdetf  22539  maduf  22585  pmatcollpw3fi1lem1  22730  chfacfisf  22798  chfacfisfcpmat  22799  cpmidpmatlem2  22815  lly1stc  23440  txcnmpt  23568  txlm  23592  xkoinjcn  23631  kqffn  23669  txflf  23950  tsmsfbas  24072  ustuqtop0  24184  metdsf  24793  metdsge  24794  mulc1cncf  24854  lebnumlem1  24916  cmetcaulem  25244  ovollb2lem  25445  ovolctb  25447  ovolunlem1a  25453  ovolunlem1  25454  ovoliunlem1  25459  ovoliunlem2  25460  ovoliun  25462  ovolshftlem1  25466  ovolscalem1  25470  ovolicc1  25473  ioombl1lem1  25515  uniioombllem2  25540  volsup2  25562  volcn  25563  vitalilem4  25568  vitalilem5  25569  mbfconst  25590  mbfmax  25606  mbfsup  25621  i1f1lem  25646  i1f1  25647  i1fres  25662  itg1climres  25671  itg2splitlem  25705  itg2split  25706  itg2monolem1  25707  itg2mono  25710  itg2i1fseq  25712  itg2i1fseq2  25713  dvreslem  25866  dvmptresicc  25873  dvivthlem1  25969  dvfsumrlimf  25987  dvfsumlem3  25991  ftc1lem2  25999  ftc1lem6  26004  radcnvlem1  26378  pserulm  26387  psercn2  26388  psercn2OLD  26389  abelthlem4  26400  efif1olem4  26510  lgamgulmlem6  27000  gamcvg  27022  basellem4  27050  basellem7  27053  basellem9  27055  lgsfcl2  27270  lgsqrlem2  27314  lgseisenlem1  27342  dchrmusum2  27461  dchrvmasumiflem1  27468  dchrisum0ff  27474  dchrisum0lem1b  27482  dchrisum0lem2a  27484  abvcxp  27582  padicabv  27597  axlowdimlem15  29029  crctcshwlkn0  29894  wlkiswwlks2lem5  29946  wlkswwlksf1o  29952  wwlksnextfun  29971  clwlkclwwlklem2a  30073  clwlkclwwlkf  30083  clwwlkf  30122  frgrncvvdeqlem4  30377  numclwwlk1lem2f  30430  numclwlk2lem2f  30452  ipblnfi  30930  ubthlem1  30945  htthlem  30992  hlimadd  31268  chscllem1  31712  cnlnadjlem2  32143  strlem3a  32327  hstrlem3a  32335  xppreima2  32729  suppovss  32760  fsuppcurry1  32803  fsuppcurry2  32804  pwrssmgc  33082  mndlactf1  33108  mndlactfo  33109  mndractf1  33110  mndractfo  33111  lmodvslmhm  33133  conjga  33252  rlocf1  33355  nsgmgc  33493  elrspunidl  33509  r1plmhm  33691  r1pquslmic  33692  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  ply1degltdimlem  33779  ply1degltdim  33780  extdgfialglem1  33849  algextdeglem8  33881  rhmpreimacnlem  34041  rhmpreimacn  34042  xrge0mulc1cn  34098  esumpcvgval  34235  esumcvg  34243  mbfmco2  34422  eulerpartlems  34517  erdszelem9  35393  cvmlift3lem3  35515  ex-sategoelel  35615  ex-sategoelelomsuc  35620  elmrsubrn  35714  mvhf  35752  iprodefisum  35935  unbdqndv1  36708  knoppf  36735  ftc1anclem3  37896  ftc1anclem5  37898  lflnegcl  39335  lshpkrcl  39376  tendo0cl  41050  primrootscoprf  42355  aks6d1c2p1  42372  aks6d1c4  42378  aks6d1c2lem4  42381  aks6d1c2  42384  aks6d1c5lem0  42389  aks6d1c5  42393  sticksstones2  42401  sticksstones8  42407  sticksstones9  42408  sticksstones10  42409  sticksstones11  42410  sticksstones12a  42411  sticksstones17  42417  sticksstones18  42418  aks6d1c6lem2  42425  aks6d1c6lem3  42426  aks6d1c6lem4  42427  aks6d1c6isolem1  42428  aks6d1c6isolem2  42429  aks6d1c6isolem3  42430  aks6d1c6lem5  42431  aks5lem2  42441  frlmsnic  42795  rhmpsr  42805  mplmapghm  42807  evlsbagval  42812  evlsmaprhm  42816  selvcllem5  42825  cantnfub  43563  binomcxplemradcnv  44593  binomcxplemcvg  44595  binomcxplemnotnn0  44597  projf1o  45441  mullimc  45862  ellimcabssub0  45863  mullimcf  45869  constlimc  45870  idlimc  45872  neglimc  45891  addlimc  45892  0ellimcdiv  45893  fnlimf  45922  liminfpnfuz  46060  xlimpnfxnegmnf2  46102  cncfshift  46118  icccncfext  46131  cncfiooiccre  46139  fprodsubrecnncnvlem  46151  fprodaddrecnncnvlem  46153  ioodvbdlimc1lem1  46175  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnxpaek  46186  dvnprodlem1  46190  itgsinexplem1  46198  itgiccshift  46224  dirkercncflem2  46348  fourierdlem4  46355  fourierdlem5  46356  fourierdlem9  46360  fourierdlem14  46365  fourierdlem16  46367  fourierdlem17  46368  fourierdlem18  46369  fourierdlem21  46372  fourierdlem22  46373  fourierdlem37  46388  fourierdlem50  46400  fourierdlem51  46401  fourierdlem53  46403  fourierdlem55  46405  fourierdlem57  46407  fourierdlem58  46408  fourierdlem59  46409  fourierdlem60  46410  fourierdlem61  46411  fourierdlem67  46417  fourierdlem68  46418  fourierdlem72  46422  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem76  46426  fourierdlem78  46428  fourierdlem80  46430  fourierdlem81  46431  fourierdlem83  46433  fourierdlem84  46434  fourierdlem88  46438  fourierdlem92  46442  fourierdlem93  46443  fourierdlem97  46447  fourierdlem101  46451  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  sqwvfoura  46472  elaa2lem  46477  etransclem1  46479  etransclem8  46486  etransclem20  46498  etransclem33  46511  etransclem35  46513  etransclem39  46517  rrxtopnfi  46531  ioorrnopnxrlem  46550  sge0tsms  46624  sge0snmpt  46627  sge0fsummpt  46634  sge0pr  46638  sge0lessmpt  46643  sge0iunmptlemfi  46657  sge0iunmptlemre  46659  sge0iunmpt  46662  sge0rpcpnf  46665  sge0isum  46671  nnfoctbdjlem  46699  psmeasure  46715  voliunsge0lem  46716  meaiuninclem  46724  meaiuninc3v  46728  meaiininclem  46730  omeiunltfirp  46763  carageniuncllem2  46766  caratheodorylem1  46770  caratheodorylem2  46771  isomenndlem  46774  hoicvr  46792  hoicvrrex  46800  ovnsupge0  46801  ovnlecvr  46802  ovnf  46807  ovn0lem  46809  ovnsubaddlem1  46814  ovnsubadd  46816  hsphoif  46820  sge0hsphoire  46833  hoidmv1lelem1  46835  hoidmv1lelem2  46836  hoidmv1lelem3  46837  hoidmv1le  46838  hoidmvlelem2  46840  hoidmvlelem3  46841  ovnhoilem1  46845  ovnsubadd2lem  46889  ovolval4lem1  46893  ovolval4lem2  46894  ovolval5lem2  46897  ovnovollem1  46900  ovnovollem2  46901  vonioolem2  46925  vonicclem2  46928  smflim  47021  nsssmfmbflem  47022  smfmullem4  47038  smfsuplem1  47055  smfsuplem3  47057  smflimsuplem3  47066  fsetsnf  47297  cfsetsnfsetf  47304  cfsetsnfsetfo  47306  imasetpreimafvbijlemf  47647  prproropf1o  47753  fmtnodvds  47790  upgrimwlklem2  48144  isubgr3stgrlem6  48217  lincvalsc0  48667  lcoc0  48668  linc0scn0  48669  linc1  48671  lincscm  48676  lincresunit3  48727  1arympt1  48884  1arymaptf  48887  2arympt  48895  2arymaptf  48898  ackendofnn0  48930  amgmlemALT  50048