Theorem fmptd 7068

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044   ↦ cmpt 5183  ⟶wf 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-fun 6501  df-fn 6502  df-f 6503

This theorem is referenced by:  fmpttd  7069  fnwelem  8087  fsetfcdm  8810  fdiagfn  8840  resixpfo  8886  xpmapenlem  9085  unxpdomlem3  9175  fsuppmptdm  9303  cantnfp1lem1  9607  cantnfp1lem2  9608  cantnfp1lem3  9609  cantnf  9622  updjudhf  9860  fseqenlem2  9954  dfac8clem  9961  coftr  10202  isf34lem2  10302  axcc2lem  10365  axdc2lem  10377  axdc3lem4  10382  pwcfsdom  10512  rpnnen1lem1  12913  tpf  14440  caucvg  15621  sumrblem  15653  summolem2a  15657  supcvg  15798  prodrblem  15871  prodmolem2a  15876  crth  16724  eulerthlem1  16727  prmreclem6  16868  4sqlem11  16902  vdwlem2  16929  vdwlem4  16931  vdwlem6  16933  vdwlem10  16937  ramub1lem2  16974  prmgaplcm  17007  frmdup1  18767  grpinvf  18894  mulgnngsum  18987  cycsubm  19110  cycsubgcl  19114  cycsubgss  19115  conjghm  19157  conjnmz  19160  qusghm  19163  galactghm  19310  symgextf  19323  symgfixf  19342  pmtrdifwrdellem1  19387  odf1  19468  dfod2  19470  pgpssslw  19520  frgpmhm  19671  gsummptfidmsplitres  19837  gsummptfidminv  19853  gsumzunsnd  19862  gsummpt1n0  19871  ablfac1b  19978  ablfac2  19997  c0mgm  20344  c0mhm  20345  c0snmgmhm  20347  abvtrivd  20717  issrngd  20740  pwssplit0  20941  rngqiprngimf  21183  mulgghm2  21362  frobrhm  21461  isphld  21539  pjff  21597  frlmup1  21683  asclf  21767  psr1cl  21846  evlslem1  21965  evlsval2  21970  evls1maprhm  22239  rhmmpl  22246  scmatf  22392  mdetf  22458  maduf  22504  pmatcollpw3fi1lem1  22649  chfacfisf  22717  chfacfisfcpmat  22718  cpmidpmatlem2  22734  lly1stc  23359  txcnmpt  23487  txlm  23511  xkoinjcn  23550  kqffn  23588  txflf  23869  tsmsfbas  23991  ustuqtop0  24104  metdsf  24713  metdsge  24714  mulc1cncf  24774  lebnumlem1  24836  cmetcaulem  25164  ovollb2lem  25365  ovolctb  25367  ovolunlem1a  25373  ovolunlem1  25374  ovoliunlem1  25379  ovoliunlem2  25380  ovoliun  25382  ovolshftlem1  25386  ovolscalem1  25390  ovolicc1  25393  ioombl1lem1  25435  uniioombllem2  25460  volsup2  25482  volcn  25483  vitalilem4  25488  vitalilem5  25489  mbfconst  25510  mbfmax  25526  mbfsup  25541  i1f1lem  25566  i1f1  25567  i1fres  25582  itg1climres  25591  itg2splitlem  25625  itg2split  25626  itg2monolem1  25627  itg2mono  25630  itg2i1fseq  25632  itg2i1fseq2  25633  dvreslem  25786  dvmptresicc  25793  dvivthlem1  25889  dvfsumrlimf  25907  dvfsumlem3  25911  ftc1lem2  25919  ftc1lem6  25924  radcnvlem1  26298  pserulm  26307  psercn2  26308  psercn2OLD  26309  abelthlem4  26320  efif1olem4  26430  lgamgulmlem6  26920  gamcvg  26942  basellem4  26970  basellem7  26973  basellem9  26975  lgsfcl2  27190  lgsqrlem2  27234  lgseisenlem1  27262  dchrmusum2  27381  dchrvmasumiflem1  27388  dchrisum0ff  27394  dchrisum0lem1b  27402  dchrisum0lem2a  27404  abvcxp  27502  padicabv  27517  axlowdimlem15  28859  crctcshwlkn0  29724  wlkiswwlks2lem5  29776  wlkswwlksf1o  29782  wwlksnextfun  29801  clwlkclwwlklem2a  29900  clwlkclwwlkf  29910  clwwlkf  29949  frgrncvvdeqlem4  30204  numclwwlk1lem2f  30257  numclwlk2lem2f  30279  ipblnfi  30757  ubthlem1  30772  htthlem  30819  hlimadd  31095  chscllem1  31539  cnlnadjlem2  31970  strlem3a  32154  hstrlem3a  32162  xppreima2  32548  suppovss  32577  fsuppcurry1  32621  fsuppcurry2  32622  pwrssmgc  32899  mndlactf1  32940  mndlactfo  32941  mndractf1  32942  mndractfo  32943  lmodvslmhm  32963  conjga  33100  rlocf1  33197  nsgmgc  33356  elrspunidl  33372  r1plmhm  33548  r1pquslmic  33549  ply1degltdimlem  33591  ply1degltdim  33592  algextdeglem8  33687  rhmpreimacnlem  33847  rhmpreimacn  33848  xrge0mulc1cn  33904  esumpcvgval  34041  esumcvg  34049  mbfmco2  34229  eulerpartlems  34324  erdszelem9  35159  cvmlift3lem3  35281  ex-sategoelel  35381  ex-sategoelelomsuc  35386  elmrsubrn  35480  mvhf  35518  iprodefisum  35701  unbdqndv1  36469  knoppf  36496  ftc1anclem3  37662  ftc1anclem5  37664  lflnegcl  39041  lshpkrcl  39082  tendo0cl  40757  primrootscoprf  42062  aks6d1c2p1  42079  aks6d1c4  42085  aks6d1c2lem4  42088  aks6d1c2  42091  aks6d1c5lem0  42096  aks6d1c5  42100  sticksstones2  42108  sticksstones8  42114  sticksstones9  42115  sticksstones10  42116  sticksstones11  42117  sticksstones12a  42118  sticksstones17  42124  sticksstones18  42125  aks6d1c6lem2  42132  aks6d1c6lem3  42133  aks6d1c6lem4  42134  aks6d1c6isolem1  42135  aks6d1c6isolem2  42136  aks6d1c6isolem3  42137  aks6d1c6lem5  42138  aks5lem2  42148  frlmsnic  42501  rhmpsr  42513  mplmapghm  42517  evlsval3  42520  evlsbagval  42527  evlsmaprhm  42531  selvcllem5  42543  cantnfub  43283  binomcxplemradcnv  44314  binomcxplemcvg  44316  binomcxplemnotnn0  44318  projf1o  45164  mullimc  45587  ellimcabssub0  45588  mullimcf  45594  constlimc  45595  idlimc  45597  neglimc  45618  addlimc  45619  0ellimcdiv  45620  fnlimf  45649  liminfpnfuz  45787  xlimpnfxnegmnf2  45829  cncfshift  45845  icccncfext  45858  cncfiooiccre  45866  fprodsubrecnncnvlem  45878  fprodaddrecnncnvlem  45880  ioodvbdlimc1lem1  45902  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  dvnxpaek  45913  dvnprodlem1  45917  itgsinexplem1  45925  itgiccshift  45951  dirkercncflem2  46075  fourierdlem4  46082  fourierdlem5  46083  fourierdlem9  46087  fourierdlem14  46092  fourierdlem16  46094  fourierdlem17  46095  fourierdlem18  46096  fourierdlem21  46099  fourierdlem22  46100  fourierdlem37  46115  fourierdlem50  46127  fourierdlem51  46128  fourierdlem53  46130  fourierdlem55  46132  fourierdlem57  46134  fourierdlem58  46135  fourierdlem59  46136  fourierdlem60  46137  fourierdlem61  46138  fourierdlem67  46144  fourierdlem68  46145  fourierdlem72  46149  fourierdlem73  46150  fourierdlem74  46151  fourierdlem75  46152  fourierdlem76  46153  fourierdlem78  46155  fourierdlem80  46157  fourierdlem81  46158  fourierdlem83  46160  fourierdlem84  46161  fourierdlem88  46165  fourierdlem92  46169  fourierdlem93  46170  fourierdlem97  46174  fourierdlem101  46178  fourierdlem103  46180  fourierdlem104  46181  fourierdlem111  46188  sqwvfoura  46199  elaa2lem  46204  etransclem1  46206  etransclem8  46213  etransclem20  46225  etransclem33  46238  etransclem35  46240  etransclem39  46244  rrxtopnfi  46258  ioorrnopnxrlem  46277  sge0tsms  46351  sge0snmpt  46354  sge0fsummpt  46361  sge0pr  46365  sge0lessmpt  46370  sge0iunmptlemfi  46384  sge0iunmptlemre  46386  sge0iunmpt  46389  sge0rpcpnf  46392  sge0isum  46398  nnfoctbdjlem  46426  psmeasure  46442  voliunsge0lem  46443  meaiuninclem  46451  meaiuninc3v  46455  meaiininclem  46457  omeiunltfirp  46490  carageniuncllem2  46493  caratheodorylem1  46497  caratheodorylem2  46498  isomenndlem  46501  hoicvr  46519  hoicvrrex  46527  ovnsupge0  46528  ovnlecvr  46529  ovnf  46534  ovn0lem  46536  ovnsubaddlem1  46541  ovnsubadd  46543  hsphoif  46547  sge0hsphoire  46560  hoidmv1lelem1  46562  hoidmv1lelem2  46563  hoidmv1lelem3  46564  hoidmv1le  46565  hoidmvlelem2  46567  hoidmvlelem3  46568  ovnhoilem1  46572  ovnsubadd2lem  46616  ovolval4lem1  46620  ovolval4lem2  46621  ovolval5lem2  46624  ovnovollem1  46627  ovnovollem2  46628  vonioolem2  46652  vonicclem2  46655  smflim  46748  nsssmfmbflem  46749  smfmullem4  46765  smfsuplem1  46782  smfsuplem3  46784  smflimsuplem3  46793  fsetsnf  47025  cfsetsnfsetf  47032  cfsetsnfsetfo  47034  imasetpreimafvbijlemf  47375  prproropf1o  47481  fmtnodvds  47518  upgrimwlklem2  47871  isubgr3stgrlem6  47943  lincvalsc0  48383  lcoc0  48384  linc0scn0  48385  linc1  48387  lincscm  48392  lincresunit3  48443  1arympt1  48600  1arymaptf  48603  2arympt  48611  2arymaptf  48614  ackendofnn0  48646  amgmlemALT  49765