Theorem fmptd 7086

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 7082	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶)
5	2, 4	sylib 218	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

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

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  fmpttd  7087  fnwelem  8110  fsetfcdm  8833  fdiagfn  8863  resixpfo  8909  xpmapenlem  9108  unxpdomlem3  9199  fsuppmptdm  9327  cantnfp1lem1  9631  cantnfp1lem2  9632  cantnfp1lem3  9633  cantnf  9646  updjudhf  9884  fseqenlem2  9978  dfac8clem  9985  coftr  10226  isf34lem2  10326  axcc2lem  10389  axdc2lem  10401  axdc3lem4  10406  pwcfsdom  10536  rpnnen1lem1  12937  tpf  14464  caucvg  15645  sumrblem  15677  summolem2a  15681  supcvg  15822  prodrblem  15895  prodmolem2a  15900  crth  16748  eulerthlem1  16751  prmreclem6  16892  4sqlem11  16926  vdwlem2  16953  vdwlem4  16955  vdwlem6  16957  vdwlem10  16961  ramub1lem2  16998  prmgaplcm  17031  frmdup1  18791  grpinvf  18918  mulgnngsum  19011  cycsubm  19134  cycsubgcl  19138  cycsubgss  19139  conjghm  19181  conjnmz  19184  qusghm  19187  galactghm  19334  symgextf  19347  symgfixf  19366  pmtrdifwrdellem1  19411  odf1  19492  dfod2  19494  pgpssslw  19544  frgpmhm  19695  gsummptfidmsplitres  19861  gsummptfidminv  19877  gsumzunsnd  19886  gsummpt1n0  19895  ablfac1b  20002  ablfac2  20021  c0mgm  20368  c0mhm  20369  c0snmgmhm  20371  abvtrivd  20741  issrngd  20764  pwssplit0  20965  rngqiprngimf  21207  mulgghm2  21386  frobrhm  21485  isphld  21563  pjff  21621  frlmup1  21707  asclf  21791  psr1cl  21870  evlslem1  21989  evlsval2  21994  evls1maprhm  22263  rhmmpl  22270  scmatf  22416  mdetf  22482  maduf  22528  pmatcollpw3fi1lem1  22673  chfacfisf  22741  chfacfisfcpmat  22742  cpmidpmatlem2  22758  lly1stc  23383  txcnmpt  23511  txlm  23535  xkoinjcn  23574  kqffn  23612  txflf  23893  tsmsfbas  24015  ustuqtop0  24128  metdsf  24737  metdsge  24738  mulc1cncf  24798  lebnumlem1  24860  cmetcaulem  25188  ovollb2lem  25389  ovolctb  25391  ovolunlem1a  25397  ovolunlem1  25398  ovoliunlem1  25403  ovoliunlem2  25404  ovoliun  25406  ovolshftlem1  25410  ovolscalem1  25414  ovolicc1  25417  ioombl1lem1  25459  uniioombllem2  25484  volsup2  25506  volcn  25507  vitalilem4  25512  vitalilem5  25513  mbfconst  25534  mbfmax  25550  mbfsup  25565  i1f1lem  25590  i1f1  25591  i1fres  25606  itg1climres  25615  itg2splitlem  25649  itg2split  25650  itg2monolem1  25651  itg2mono  25654  itg2i1fseq  25656  itg2i1fseq2  25657  dvreslem  25810  dvmptresicc  25817  dvivthlem1  25913  dvfsumrlimf  25931  dvfsumlem3  25935  ftc1lem2  25943  ftc1lem6  25948  radcnvlem1  26322  pserulm  26331  psercn2  26332  psercn2OLD  26333  abelthlem4  26344  efif1olem4  26454  lgamgulmlem6  26944  gamcvg  26966  basellem4  26994  basellem7  26997  basellem9  26999  lgsfcl2  27214  lgsqrlem2  27258  lgseisenlem1  27286  dchrmusum2  27405  dchrvmasumiflem1  27412  dchrisum0ff  27418  dchrisum0lem1b  27426  dchrisum0lem2a  27428  abvcxp  27526  padicabv  27541  axlowdimlem15  28883  crctcshwlkn0  29751  wlkiswwlks2lem5  29803  wlkswwlksf1o  29809  wwlksnextfun  29828  clwlkclwwlklem2a  29927  clwlkclwwlkf  29937  clwwlkf  29976  frgrncvvdeqlem4  30231  numclwwlk1lem2f  30284  numclwlk2lem2f  30306  ipblnfi  30784  ubthlem1  30799  htthlem  30846  hlimadd  31122  chscllem1  31566  cnlnadjlem2  31997  strlem3a  32181  hstrlem3a  32189  xppreima2  32575  suppovss  32604  fsuppcurry1  32648  fsuppcurry2  32649  pwrssmgc  32926  mndlactf1  32967  mndlactfo  32968  mndractf1  32969  mndractfo  32970  lmodvslmhm  32990  conjga  33127  rlocf1  33224  nsgmgc  33383  elrspunidl  33399  r1plmhm  33575  r1pquslmic  33576  ply1degltdimlem  33618  ply1degltdim  33619  algextdeglem8  33714  rhmpreimacnlem  33874  rhmpreimacn  33875  xrge0mulc1cn  33931  esumpcvgval  34068  esumcvg  34076  mbfmco2  34256  eulerpartlems  34351  erdszelem9  35186  cvmlift3lem3  35308  ex-sategoelel  35408  ex-sategoelelomsuc  35413  elmrsubrn  35507  mvhf  35545  iprodefisum  35728  unbdqndv1  36496  knoppf  36523  ftc1anclem3  37689  ftc1anclem5  37691  lflnegcl  39068  lshpkrcl  39109  tendo0cl  40784  primrootscoprf  42089  aks6d1c2p1  42106  aks6d1c4  42112  aks6d1c2lem4  42115  aks6d1c2  42118  aks6d1c5lem0  42123  aks6d1c5  42127  sticksstones2  42135  sticksstones8  42141  sticksstones9  42142  sticksstones10  42143  sticksstones11  42144  sticksstones12a  42145  sticksstones17  42151  sticksstones18  42152  aks6d1c6lem2  42159  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c6isolem1  42162  aks6d1c6isolem2  42163  aks6d1c6isolem3  42164  aks6d1c6lem5  42165  aks5lem2  42175  frlmsnic  42528  rhmpsr  42540  mplmapghm  42544  evlsval3  42547  evlsbagval  42554  evlsmaprhm  42558  selvcllem5  42570  cantnfub  43310  binomcxplemradcnv  44341  binomcxplemcvg  44343  binomcxplemnotnn0  44345  projf1o  45191  mullimc  45614  ellimcabssub0  45615  mullimcf  45621  constlimc  45622  idlimc  45624  neglimc  45645  addlimc  45646  0ellimcdiv  45647  fnlimf  45676  liminfpnfuz  45814  xlimpnfxnegmnf2  45856  cncfshift  45872  icccncfext  45885  cncfiooiccre  45893  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnxpaek  45940  dvnprodlem1  45944  itgsinexplem1  45952  itgiccshift  45978  dirkercncflem2  46102  fourierdlem4  46109  fourierdlem5  46110  fourierdlem9  46114  fourierdlem14  46119  fourierdlem16  46121  fourierdlem17  46122  fourierdlem18  46123  fourierdlem21  46126  fourierdlem22  46127  fourierdlem37  46142  fourierdlem50  46154  fourierdlem51  46155  fourierdlem53  46157  fourierdlem55  46159  fourierdlem57  46161  fourierdlem58  46162  fourierdlem59  46163  fourierdlem60  46164  fourierdlem61  46165  fourierdlem67  46171  fourierdlem68  46172  fourierdlem72  46176  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem78  46182  fourierdlem80  46184  fourierdlem81  46185  fourierdlem83  46187  fourierdlem84  46188  fourierdlem88  46192  fourierdlem92  46196  fourierdlem93  46197  fourierdlem97  46201  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  sqwvfoura  46226  elaa2lem  46231  etransclem1  46233  etransclem8  46240  etransclem20  46252  etransclem33  46265  etransclem35  46267  etransclem39  46271  rrxtopnfi  46285  ioorrnopnxrlem  46304  sge0tsms  46378  sge0snmpt  46381  sge0fsummpt  46388  sge0pr  46392  sge0lessmpt  46397  sge0iunmptlemfi  46411  sge0iunmptlemre  46413  sge0iunmpt  46416  sge0rpcpnf  46419  sge0isum  46425  nnfoctbdjlem  46453  psmeasure  46469  voliunsge0lem  46470  meaiuninclem  46478  meaiuninc3v  46482  meaiininclem  46484  omeiunltfirp  46517  carageniuncllem2  46520  caratheodorylem1  46524  caratheodorylem2  46525  isomenndlem  46528  hoicvr  46546  hoicvrrex  46554  ovnsupge0  46555  ovnlecvr  46556  ovnf  46561  ovn0lem  46563  ovnsubaddlem1  46568  ovnsubadd  46570  hsphoif  46574  sge0hsphoire  46587  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmv1le  46592  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnhoilem1  46599  ovnsubadd2lem  46643  ovolval4lem1  46647  ovolval4lem2  46648  ovolval5lem2  46651  ovnovollem1  46654  ovnovollem2  46655  vonioolem2  46679  vonicclem2  46682  smflim  46775  nsssmfmbflem  46776  smfmullem4  46792  smfsuplem1  46809  smfsuplem3  46811  smflimsuplem3  46820  fsetsnf  47052  cfsetsnfsetf  47059  cfsetsnfsetfo  47061  imasetpreimafvbijlemf  47402  prproropf1o  47508  fmtnodvds  47545  upgrimwlklem2  47898  isubgr3stgrlem6  47970  lincvalsc0  48410  lcoc0  48411  linc0scn0  48412  linc1  48414  lincscm  48419  lincresunit3  48470  1arympt1  48627  1arymaptf  48630  2arympt  48638  2arymaptf  48641  ackendofnn0  48673  amgmlemALT  49792