Theorem fmptd 7113

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∀wral 3081   ↦ cmpt 5194  ⟶wf 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6542  df-fn 6543  df-f 6544

This theorem is used by:  fmpttd  7114  fnwelem  8133  fsetfcdm  8863  fdiagfn  8894  resixpfo  8940  xpmapenlem  9139  unxpdomlem3  9225  fsuppmptdm  9343  cantnfp1lem1  9654  cantnfp1lem2  9655  cantnfp1lem3  9656  cantnf  9669  updjudhf  9933  fseqenlem2  10025  dfac8clem  10032  coftr  10272  isf34lem2  10372  axcc2lem  10435  axdc2lem  10447  axdc3lem4  10452  pwcfsdom  10583  rpnnen1lem1  13018  tpf  14554  caucvg  15754  sumrblem  15785  summolem2a  15789  supcvg  15933  prodrblem  16006  prodmolem2a  16011  crth  16859  eulerthlem1  16862  prmreclem6  17003  4sqlem11  17037  vdwlem2  17064  vdwlem4  17066  vdwlem6  17068  vdwlem10  17072  ramub1lem2  17109  prmgaplcm  17142  frmdup1  18960  grpinvf  19097  mulgnngsum  19189  cycsubm  19317  cycsubgcl  19321  cycsubgss  19322  conjghm  19363  conjnmz  19366  qusghm  19369  galactghm  19518  symgextf  19531  symgfixf  19550  pmtrdifwrdellem1  19595  odf1  19676  dfod2  19678  pgpssslw  19728  frgpmhm  19879  gsummptfidmsplitres  20045  gsummptfidminv  20061  gsumzunsnd  20070  gsummpt1n0  20079  ablfac1b  20186  ablfac2  20205  c0mgm  20587  c0mhm  20588  c0snmgmhm  20590  abvtrivd  20985  issrngd  21008  pwssplit0  21229  rngqiprngimf  21487  mulgghm2  21676  frobrhm  21775  isphld  21854  pjff  21912  frlmup1  21998  asclf  22081  psr1cl  22160  evlslem1  22283  evlsval2  22288  evlsval3  22290  mplmapghm  22323  evlsmaprhm  22332  selvcllem5  22340  evls1maprhm  22586  rhmmpl  22590  scmatf  22736  mdetf  22802  maduf  22848  pmatcollpw3fi1lem1  22993  chfacfisf  23061  chfacfisfcpmat  23062  cpmidpmatlem2  23078  lly1stc  23704  txcnmpt  23832  txlm  23856  xkoinjcn  23895  kqffn  23933  txflf  24214  tsmsfbas  24336  ustuqtop0  24448  metdsf  25057  metdsge  25058  mulc1cncf  25115  lebnumlem1  25171  cmetcaulem  25498  ovollb2lem  25698  ovolctb  25700  ovolunlem1a  25706  ovolunlem1  25707  ovoliunlem1  25712  ovoliunlem2  25713  ovoliun  25715  ovolshftlem1  25719  ovolscalem1  25723  ovolicc1  25726  ioombl1lem1  25768  uniioombllem2  25793  volsup2  25815  volcn  25816  vitalilem4  25821  vitalilem5  25822  mbfconst  25843  mbfmax  25859  mbfsup  25874  i1f1lem  25899  i1f1  25900  i1fres  25915  itg1climres  25924  itg2splitlem  25958  itg2split  25959  itg2monolem1  25960  itg2mono  25963  itg2i1fseq  25965  itg2i1fseq2  25966  dvreslem  26119  dvmptresicc  26126  dvivthlem1  26218  dvfsumrlimf  26235  dvfsumlem3  26238  ftc1lem2  26246  ftc1lem6  26251  radcnvlem1  26627  pserulm  26636  psercn2  26637  abelthlem4  26648  efif1olem4  26761  lgamgulmlem6  27249  gamcvg  27271  basellem4  27299  basellem7  27302  basellem9  27304  lgsfcl2  27518  lgsqrlem2  27562  lgseisenlem1  27590  dchrmusum2  27709  dchrvmasumiflem1  27716  dchrisum0ff  27722  dchrisum0lem1b  27730  dchrisum0lem2a  27732  abvcxp  27830  padicabv  27845  axlowdimlem15  29361  crctcshwlkn0  30237  wlkiswwlks2lem5  30289  wlkswwlksf1o  30295  wwlksnextfun  30314  clwlkclwwlklem2a  30416  clwlkclwwlkf  30426  clwwlkf  30465  frgrncvvdeqlem4  30724  numclwwlk1lem2f  30777  numclwlk2lem2f  30799  ipblnfi  31278  ubthlem1  31293  htthlem  31340  hlimadd  31616  chscllem1  32060  cnlnadjlem2  32491  strlem3a  32675  hstrlem3a  32683  xppreima2  33067  suppovss  33097  fsuppcurry1  33139  fsuppcurry2  33140  pwrssmgc  33384  mndlactf1  33410  mndlactfo  33411  mndractf1  33412  mndractfo  33413  lmodvslmhm  33434  conjga  33554  rlocf1  33658  nsgmgc  33785  elrspunidl  33800  r1plmhm  33963  r1pquslmic  33964  selvply1rhmlem1  33974  mplvrpmga  33999  mplvrpmmhm  34000  mplvrpmrhm  34001  psrmonprod  34006  mplmonprod  34008  ply1degltdimlem  34076  ply1degltdim  34077  extdgfialglem1  34146  algextdeglem8  34178  rhmpreimacnlem  34338  rhmpreimacn  34339  xrge0mulc1cn  34395  esumpcvgval  34532  esumcvg  34540  mbfmco2  34720  eulerpartlems  34815  onvfowev  35657  erdszelem9  35728  cvmlift3lem3  35850  ex-sategoelel  35950  ex-sategoelelomsuc  35955  elmrsubrn  36049  mvhf  36087  iprodefisum  36270  unbdqndv1  37154  knoppf  37181  ftc1anclem3  38403  ftc1anclem5  38405  lflnegcl  39907  lshpkrcl  39948  tendo0cl  41622  primrootscoprf  42926  aks6d1c2p1  42943  aks6d1c4  42949  aks6d1c2lem4  42952  aks6d1c2  42955  aks6d1c5lem0  42960  aks6d1c5  42964  sticksstones2  42972  sticksstones8  42978  sticksstones9  42979  sticksstones10  42980  sticksstones11  42981  sticksstones12a  42982  sticksstones17  42988  sticksstones18  42989  aks6d1c6lem2  42996  aks6d1c6lem3  42997  aks6d1c6lem4  42998  aks6d1c6isolem1  42999  aks6d1c6isolem2  43000  aks6d1c6isolem3  43001  aks6d1c6lem5  43002  aks5lem2  43012  frlmsnic  43366  rhmpsr  43373  evlsbagval  43376  cantnfub  44106  binomcxplemradcnv  45120  binomcxplemcvg  45122  binomcxplemnotnn0  45124  projf1o  45972  mullimc  46390  ellimcabssub0  46391  mullimcf  46397  constlimc  46398  idlimc  46400  neglimc  46419  addlimc  46420  0ellimcdiv  46421  fnlimf  46450  liminfpnfuz  46588  xlimpnfxnegmnf2  46630  cncfshift  46646  icccncfext  46659  cncfiooiccre  46667  fprodsubrecnncnvlem  46679  fprodaddrecnncnvlem  46681  ioodvbdlimc1lem1  46703  ioodvbdlimc1lem2  46704  ioodvbdlimc2lem  46706  dvnxpaek  46714  dvnprodlem1  46718  itgsinexplem1  46726  itgiccshift  46752  dirkercncflem2  46876  fourierdlem4  46883  fourierdlem5  46884  fourierdlem9  46888  fourierdlem14  46893  fourierdlem16  46895  fourierdlem17  46896  fourierdlem18  46897  fourierdlem21  46900  fourierdlem22  46901  fourierdlem37  46916  fourierdlem50  46928  fourierdlem51  46929  fourierdlem53  46931  fourierdlem55  46933  fourierdlem57  46935  fourierdlem58  46936  fourierdlem59  46937  fourierdlem60  46938  fourierdlem61  46939  fourierdlem67  46945  fourierdlem68  46946  fourierdlem72  46950  fourierdlem73  46951  fourierdlem74  46952  fourierdlem75  46953  fourierdlem76  46954  fourierdlem78  46956  fourierdlem80  46958  fourierdlem81  46959  fourierdlem83  46961  fourierdlem84  46962  fourierdlem88  46966  fourierdlem92  46970  fourierdlem93  46971  fourierdlem97  46975  fourierdlem101  46979  fourierdlem103  46981  fourierdlem104  46982  fourierdlem111  46989  sqwvfoura  47000  elaa2lem  47005  etransclem1  47007  etransclem8  47014  etransclem20  47026  etransclem33  47039  etransclem35  47041  etransclem39  47045  rrxtopnfi  47059  ioorrnopnxrlem  47078  sge0tsms  47152  sge0snmpt  47155  sge0fsummpt  47162  sge0pr  47166  sge0lessmpt  47171  sge0iunmptlemfi  47185  sge0iunmptlemre  47187  sge0iunmpt  47190  sge0rpcpnf  47193  sge0isum  47199  nnfoctbdjlem  47227  psmeasure  47243  voliunsge0lem  47244  meaiuninclem  47252  meaiuninc3v  47256  meaiininclem  47258  omeiunltfirp  47291  carageniuncllem2  47294  caratheodorylem1  47298  caratheodorylem2  47299  isomenndlem  47302  hoicvrrex  47328  ovnsupge0  47329  ovnlecvr  47330  ovnf  47335  ovn0lem  47337  ovnsubaddlem1  47342  ovnsubadd  47344  hsphoif  47348  sge0hsphoire  47361  hoidmv1lelem1  47363  hoidmv1lelem2  47364  hoidmv1lelem3  47365  hoidmv1le  47366  hoidmvlelem2  47368  hoidmvlelem3  47369  ovnhoilem1  47373  ovnsubadd2lem  47417  ovolval4lem1  47421  ovolval4lem2  47422  ovolval5lem2  47425  ovnovollem1  47428  ovnovollem2  47429  vonioolem2  47453  vonicclem2  47456  smflim  47549  nsssmfmbflem  47550  smfmullem4  47566  smfsuplem1  47583  smfsuplem3  47585  smflimsuplem3  47594  fsetsnf  47846  cfsetsnfsetf  47853  cfsetsnfsetfo  47855  imasetpreimafvbijlemf  48208  prproropf1o  48314  fmtnodvds  48354  upgrimwlklem2  48721  isubgr3stgrlem6  48794  lincvalsc0  49258  lcoc0  49259  linc0scn0  49260  linc1  49262  lincscm  49267  lincresunit3  49318  1arympt1  49475  1arymaptf  49478  2arympt  49486  2arymaptf  49489  ackendofnn0  49521  amgmlemALT  50708