Theorem fmptd 7066

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3051   ↦ cmpt 5166  ⟶wf 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-mpt 5167  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 6500  df-fn 6501  df-f 6502

This theorem is referenced by:  fmpttd  7067  fnwelem  8081  fsetfcdm  8807  fdiagfn  8838  resixpfo  8884  xpmapenlem  9082  unxpdomlem3  9168  fsuppmptdm  9289  cantnfp1lem1  9599  cantnfp1lem2  9600  cantnfp1lem3  9601  cantnf  9614  updjudhf  9855  fseqenlem2  9947  dfac8clem  9954  coftr  10195  isf34lem2  10295  axcc2lem  10358  axdc2lem  10370  axdc3lem4  10375  pwcfsdom  10506  rpnnen1lem1  12928  tpf  14461  caucvg  15641  sumrblem  15673  summolem2a  15677  supcvg  15821  prodrblem  15894  prodmolem2a  15899  crth  16748  eulerthlem1  16751  prmreclem6  16892  4sqlem11  16926  vdwlem2  16953  vdwlem4  16955  vdwlem6  16957  vdwlem10  16961  ramub1lem2  16998  prmgaplcm  17031  frmdup1  18832  grpinvf  18962  mulgnngsum  19055  cycsubm  19177  cycsubgcl  19181  cycsubgss  19182  conjghm  19224  conjnmz  19227  qusghm  19230  galactghm  19379  symgextf  19392  symgfixf  19411  pmtrdifwrdellem1  19456  odf1  19537  dfod2  19539  pgpssslw  19589  frgpmhm  19740  gsummptfidmsplitres  19906  gsummptfidminv  19922  gsumzunsnd  19931  gsummpt1n0  19940  ablfac1b  20047  ablfac2  20066  c0mgm  20439  c0mhm  20440  c0snmgmhm  20442  abvtrivd  20809  issrngd  20832  pwssplit0  21053  rngqiprngimf  21295  mulgghm2  21456  frobrhm  21555  isphld  21634  pjff  21692  frlmup1  21778  asclf  21861  psr1cl  21939  evlslem1  22060  evlsval2  22065  evlsval3  22067  evls1maprhm  22341  rhmmpl  22348  scmatf  22494  mdetf  22560  maduf  22606  pmatcollpw3fi1lem1  22751  chfacfisf  22819  chfacfisfcpmat  22820  cpmidpmatlem2  22836  lly1stc  23461  txcnmpt  23589  txlm  23613  xkoinjcn  23652  kqffn  23690  txflf  23971  tsmsfbas  24093  ustuqtop0  24205  metdsf  24814  metdsge  24815  mulc1cncf  24872  lebnumlem1  24928  cmetcaulem  25255  ovollb2lem  25455  ovolctb  25457  ovolunlem1a  25463  ovolunlem1  25464  ovoliunlem1  25469  ovoliunlem2  25470  ovoliun  25472  ovolshftlem1  25476  ovolscalem1  25480  ovolicc1  25483  ioombl1lem1  25525  uniioombllem2  25550  volsup2  25572  volcn  25573  vitalilem4  25578  vitalilem5  25579  mbfconst  25600  mbfmax  25616  mbfsup  25631  i1f1lem  25656  i1f1  25657  i1fres  25672  itg1climres  25681  itg2splitlem  25715  itg2split  25716  itg2monolem1  25717  itg2mono  25720  itg2i1fseq  25722  itg2i1fseq2  25723  dvreslem  25876  dvmptresicc  25883  dvivthlem1  25975  dvfsumrlimf  25992  dvfsumlem3  25995  ftc1lem2  26003  ftc1lem6  26008  radcnvlem1  26378  pserulm  26387  psercn2  26388  abelthlem4  26399  efif1olem4  26509  lgamgulmlem6  26997  gamcvg  27019  basellem4  27047  basellem7  27050  basellem9  27052  lgsfcl2  27266  lgsqrlem2  27310  lgseisenlem1  27338  dchrmusum2  27457  dchrvmasumiflem1  27464  dchrisum0ff  27470  dchrisum0lem1b  27478  dchrisum0lem2a  27480  abvcxp  27578  padicabv  27593  axlowdimlem15  29025  crctcshwlkn0  29889  wlkiswwlks2lem5  29941  wlkswwlksf1o  29947  wwlksnextfun  29966  clwlkclwwlklem2a  30068  clwlkclwwlkf  30078  clwwlkf  30117  frgrncvvdeqlem4  30372  numclwwlk1lem2f  30425  numclwlk2lem2f  30447  ipblnfi  30926  ubthlem1  30941  htthlem  30988  hlimadd  31264  chscllem1  31708  cnlnadjlem2  32139  strlem3a  32323  hstrlem3a  32331  xppreima2  32724  suppovss  32754  fsuppcurry1  32797  fsuppcurry2  32798  pwrssmgc  33060  mndlactf1  33086  mndlactfo  33087  mndractf1  33088  mndractfo  33089  lmodvslmhm  33111  conjga  33231  rlocf1  33334  nsgmgc  33472  elrspunidl  33488  r1plmhm  33670  r1pquslmic  33671  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  psrmonprod  33696  mplmonprod  33698  ply1degltdimlem  33766  ply1degltdim  33767  extdgfialglem1  33836  algextdeglem8  33868  rhmpreimacnlem  34028  rhmpreimacn  34029  xrge0mulc1cn  34085  esumpcvgval  34222  esumcvg  34230  mbfmco2  34409  eulerpartlems  34504  erdszelem9  35381  cvmlift3lem3  35503  ex-sategoelel  35603  ex-sategoelelomsuc  35608  elmrsubrn  35702  mvhf  35740  iprodefisum  35923  unbdqndv1  36768  knoppf  36795  ftc1anclem3  38016  ftc1anclem5  38018  lflnegcl  39521  lshpkrcl  39562  tendo0cl  41236  primrootscoprf  42540  aks6d1c2p1  42557  aks6d1c4  42563  aks6d1c2lem4  42566  aks6d1c2  42569  aks6d1c5lem0  42574  aks6d1c5  42578  sticksstones2  42586  sticksstones8  42592  sticksstones9  42593  sticksstones10  42594  sticksstones11  42595  sticksstones12a  42596  sticksstones17  42602  sticksstones18  42603  aks6d1c6lem2  42610  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c6isolem1  42613  aks6d1c6isolem2  42614  aks6d1c6isolem3  42615  aks6d1c6lem5  42616  aks5lem2  42626  frlmsnic  42985  rhmpsr  42995  mplmapghm  42997  evlsbagval  43002  evlsmaprhm  43006  selvcllem5  43015  cantnfub  43749  binomcxplemradcnv  44779  binomcxplemcvg  44781  binomcxplemnotnn0  44783  projf1o  45626  mullimc  46046  ellimcabssub0  46047  mullimcf  46053  constlimc  46054  idlimc  46056  neglimc  46075  addlimc  46076  0ellimcdiv  46077  fnlimf  46106  liminfpnfuz  46244  xlimpnfxnegmnf2  46286  cncfshift  46302  icccncfext  46315  cncfiooiccre  46323  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnxpaek  46370  dvnprodlem1  46374  itgsinexplem1  46382  itgiccshift  46408  dirkercncflem2  46532  fourierdlem4  46539  fourierdlem5  46540  fourierdlem9  46544  fourierdlem14  46549  fourierdlem16  46551  fourierdlem17  46552  fourierdlem18  46553  fourierdlem21  46556  fourierdlem22  46557  fourierdlem37  46572  fourierdlem50  46584  fourierdlem51  46585  fourierdlem53  46587  fourierdlem55  46589  fourierdlem57  46591  fourierdlem58  46592  fourierdlem59  46593  fourierdlem60  46594  fourierdlem61  46595  fourierdlem67  46601  fourierdlem68  46602  fourierdlem72  46606  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem78  46612  fourierdlem80  46614  fourierdlem81  46615  fourierdlem83  46617  fourierdlem84  46618  fourierdlem88  46622  fourierdlem92  46626  fourierdlem93  46627  fourierdlem97  46631  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  sqwvfoura  46656  elaa2lem  46661  etransclem1  46663  etransclem8  46670  etransclem20  46682  etransclem33  46695  etransclem35  46697  etransclem39  46701  rrxtopnfi  46715  ioorrnopnxrlem  46734  sge0tsms  46808  sge0snmpt  46811  sge0fsummpt  46818  sge0pr  46822  sge0lessmpt  46827  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0iunmpt  46846  sge0rpcpnf  46849  sge0isum  46855  nnfoctbdjlem  46883  psmeasure  46899  voliunsge0lem  46900  meaiuninclem  46908  meaiuninc3v  46912  meaiininclem  46914  omeiunltfirp  46947  carageniuncllem2  46950  caratheodorylem1  46954  caratheodorylem2  46955  isomenndlem  46958  hoicvrrex  46984  ovnsupge0  46985  ovnlecvr  46986  ovnf  46991  ovn0lem  46993  ovnsubaddlem1  46998  ovnsubadd  47000  hsphoif  47004  sge0hsphoire  47017  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmv1le  47022  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnhoilem1  47029  ovnsubadd2lem  47073  ovolval4lem1  47077  ovolval4lem2  47078  ovolval5lem2  47081  ovnovollem1  47084  ovnovollem2  47085  vonioolem2  47109  vonicclem2  47112  smflim  47205  nsssmfmbflem  47206  smfmullem4  47222  smfsuplem1  47239  smfsuplem3  47241  smflimsuplem3  47250  fsetsnf  47499  cfsetsnfsetf  47506  cfsetsnfsetfo  47508  imasetpreimafvbijlemf  47861  prproropf1o  47967  fmtnodvds  48007  upgrimwlklem2  48374  isubgr3stgrlem6  48447  lincvalsc0  48897  lcoc0  48898  linc0scn0  48899  linc1  48901  lincscm  48906  lincresunit3  48957  1arympt1  49114  1arymaptf  49117  2arympt  49125  2arymaptf  49128  ackendofnn0  49160  amgmlemALT  50278