Theorem fmptd 7146

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∀wral 3080   ↦ cmpt 5192  ⟶wf 6562

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-pr 5398

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-fun 6568  df-fn 6569  df-f 6570

This theorem is used by:  fmpttd  7147  fnwelem  8180  fsetfcdm  8920  fdiagfn  8956  resixpfo  9002  xpmapenlem  9201  unxpdomlem3  9287  fsuppmptdm  9405  cantnfp1lem1  9716  cantnfp1lem2  9717  cantnfp1lem3  9718  cantnf  9731  updjudhf  10049  fseqenlem2  10143  dfac8clem  10150  coftr  10390  isf34lem2  10490  axcc2lem  10553  axdc2lem  10565  axdc3lem4  10570  pwcfsdom  10707  rpnnen1lem1  13146  tpf  14685  caucvg  15890  sumrblem  15921  summolem2a  15925  supcvg  16069  prodrblem  16140  prodmolem2a  16145  crth  16999  eulerthlem1  17002  prmreclem6  17143  4sqlem11  17177  vdwlem2  17204  vdwlem4  17206  vdwlem6  17208  vdwlem10  17212  ramub1lem2  17249  prmgaplcm  17282  frmdup1  19110  grpinvf  19247  mulgnngsum  19339  cycsubm  19467  cycsubgcl  19471  cycsubgss  19472  conjghm  19513  conjnmz  19516  qusghm  19519  galactghm  19669  symgextf  19682  symgfixf  19701  pmtrdifwrdellem1  19746  odf1  19827  dfod2  19829  pgpssslw  19879  frgpmhm  20030  gsummptfidmsplitres  20196  gsummptfidminv  20212  gsumzunsnd  20221  gsummpt1n0  20230  ablfac1b  20337  ablfac2  20356  c0mgm  20740  c0mhm  20741  c0snmgmhm  20743  abvtrivd  21140  issrngd  21163  pwssplit0  21384  rngqiprngimf  21644  mulgghm2  21837  frobrhm  21936  isphld  22015  pjff  22073  frlmup1  22159  asclf  22244  psr1cl  22323  evlslem1  22446  evlsval2  22451  evlsval3  22453  mplmapghm  22486  evlsmaprhm  22495  selvcllem5  22503  evls1maprhm  22749  rhmmpl  22753  scmatf  22899  mdetf  22965  maduf  23011  pmatcollpw3fi1lem1  23159  chfacfisf  23227  chfacfisfcpmat  23228  cpmidpmatlem2  23244  lly1stc  23870  txcnmpt  23998  txlm  24022  xkoinjcn  24061  kqffn  24099  txflf  24380  tsmsfbas  24502  ustuqtop0  24614  metdsf  25223  metdsge  25224  mulc1cncf  25281  lebnumlem1  25337  cmetcaulem  25664  ovollb2lem  25864  ovolctb  25866  ovolunlem1a  25872  ovolunlem1  25873  ovoliunlem1  25878  ovoliunlem2  25879  ovoliun  25881  ovolshftlem1  25885  ovolscalem1  25889  ovolicc1  25892  ioombl1lem1  25934  uniioombllem2  25959  volsup2  25981  volcn  25982  vitalilem4  25987  vitalilem5  25988  mbfconst  26009  mbfmax  26025  mbfsup  26040  i1f1lem  26065  i1f1  26066  i1fres  26081  itg1climres  26090  itg2splitlem  26124  itg2split  26125  itg2monolem1  26126  itg2mono  26129  itg2i1fseq  26131  itg2i1fseq2  26132  dvreslem  26284  dvmptresicc  26291  dvivthlem1  26383  dvfsumrlimf  26400  dvfsumlem3  26403  ftc1lem2  26411  ftc1lem6  26416  radcnvlem1  26797  pserulm  26806  psercn2  26807  abelthlem4  26818  efif1olem4  26930  lgamgulmlem6  27418  gamcvg  27440  basellem4  27468  basellem7  27471  basellem9  27473  lgsfcl2  27687  lgsqrlem2  27731  lgseisenlem1  27759  dchrmusum2  27878  dchrvmasumiflem1  27885  dchrisum0ff  27891  dchrisum0lem1b  27899  dchrisum0lem2a  27901  abvcxp  27999  padicabv  28014  axlowdimlem15  29591  crctcshwlkn0  30467  wlkiswwlks2lem5  30519  wlkswwlksf1o  30525  wwlksnextfun  30544  clwlkclwwlklem2a  30646  clwlkclwwlkf  30656  clwwlkf  30695  frgrncvvdeqlem4  30960  numclwwlk1lem2f  31013  numclwlk2lem2f  31035  ipblnfi  31514  ubthlem1  31529  htthlem  31576  hlimadd  31852  chscllem1  32296  cnlnadjlem2  32727  strlem3a  32911  hstrlem3a  32919  xppreima2  33343  suppovss  33371  fsuppcurry1  33412  fsuppcurry2  33413  pwrssmgc  33660  mndlactf1  33686  mndlactfo  33687  mndractf1  33688  mndractfo  33689  lmodvslmhm  33710  conjga  33830  rlocf1  33934  nsgmgc  34067  elrspunidl  34082  r1plmhm  34246  r1pquslmic  34247  selvply1rhmlem1  34263  mplvrpmga  34288  mplvrpmmhm  34289  mplvrpmrhm  34290  psrmonprod  34295  mplmonprod  34297  ply1degltdimlem  34365  ply1degltdim  34366  extdgfialglem1  34435  algextdeglem8  34467  rhmpreimacnlem  34627  rhmpreimacn  34628  xrge0mulc1cn  34684  esumpcvgval  34821  esumcvg  34829  mbfmco2  35008  eulerpartlems  35103  onvfowev  36091  erdszelem9  36172  cvmlift3lem3  36294  ex-sategoelel  36394  ex-sategoelelomsuc  36399  elmrsubrn  36493  mvhf  36531  iprodefisum  36721  unbdqndv1  37589  knoppf  37616  ftc1anclem3  38881  ftc1anclem5  38883  lflnegcl  40398  lshpkrcl  40439  tendo0cl  42113  primrootscoprf  43417  aks6d1c2p1  43434  aks6d1c4  43440  aks6d1c2lem4  43443  aks6d1c2  43446  aks6d1c5lem0  43451  aks6d1c5  43455  sticksstones2  43463  sticksstones8  43469  sticksstones9  43470  sticksstones10  43471  sticksstones11  43472  sticksstones12a  43473  sticksstones17  43479  sticksstones18  43480  aks6d1c6lem2  43487  aks6d1c6lem3  43488  aks6d1c6lem4  43489  aks6d1c6isolem1  43490  aks6d1c6isolem2  43491  aks6d1c6isolem3  43492  aks6d1c6lem5  43493  aks5lem2  43503  frlmsnic  43870  rhmpsr  43877  evlsbagval  43880  cantnfub  44584  binomcxplemradcnv  45597  binomcxplemcvg  45599  binomcxplemnotnn0  45601  projf1o  46484  mullimc  46901  ellimcabssub0  46902  mullimcf  46908  constlimc  46909  idlimc  46911  neglimc  46930  addlimc  46931  0ellimcdiv  46932  fnlimf  46961  liminfpnfuz  47099  xlimpnfxnegmnf2  47141  cncfshift  47157  icccncfext  47170  cncfiooiccre  47178  fprodsubrecnncnvlem  47190  fprodaddrecnncnvlem  47192  ioodvbdlimc1lem1  47214  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnxpaek  47225  dvnprodlem1  47229  itgsinexplem1  47237  itgiccshift  47263  dirkercncflem2  47387  fourierdlem4  47394  fourierdlem5  47395  fourierdlem9  47399  fourierdlem14  47404  fourierdlem16  47406  fourierdlem17  47407  fourierdlem18  47408  fourierdlem21  47411  fourierdlem22  47412  fourierdlem37  47427  fourierdlem50  47439  fourierdlem51  47440  fourierdlem53  47442  fourierdlem55  47444  fourierdlem57  47446  fourierdlem58  47447  fourierdlem59  47448  fourierdlem60  47449  fourierdlem61  47450  fourierdlem67  47456  fourierdlem68  47457  fourierdlem72  47461  fourierdlem73  47462  fourierdlem74  47463  fourierdlem75  47464  fourierdlem76  47465  fourierdlem78  47467  fourierdlem80  47469  fourierdlem81  47470  fourierdlem83  47472  fourierdlem84  47473  fourierdlem88  47477  fourierdlem92  47481  fourierdlem93  47482  fourierdlem97  47486  fourierdlem101  47490  fourierdlem103  47492  fourierdlem104  47493  fourierdlem111  47500  sqwvfoura  47511  elaa2lem  47516  etransclem1  47518  etransclem8  47525  etransclem20  47537  etransclem33  47550  etransclem35  47552  etransclem39  47556  rrxtopnfi  47570  ioorrnopnxrlem  47589  sge0tsms  47663  sge0snmpt  47666  sge0fsummpt  47673  sge0pr  47677  sge0lessmpt  47682  sge0iunmptlemfi  47696  sge0iunmptlemre  47698  sge0iunmpt  47701  sge0rpcpnf  47704  sge0isum  47710  nnfoctbdjlem  47738  psmeasure  47754  voliunsge0lem  47755  meaiuninclem  47763  meaiuninc3v  47767  meaiininclem  47769  omeiunltfirp  47802  carageniuncllem2  47805  caratheodorylem1  47809  caratheodorylem2  47810  isomenndlem  47813  hoicvrrex  47839  ovnsupge0  47840  ovnlecvr  47841  ovnf  47846  ovn0lem  47848  ovnsubaddlem1  47853  ovnsubadd  47855  hsphoif  47859  sge0hsphoire  47872  hoidmv1lelem1  47874  hoidmv1lelem2  47875  hoidmv1lelem3  47876  hoidmv1le  47877  hoidmvlelem2  47879  hoidmvlelem3  47880  ovnhoilem1  47884  ovnsubadd2lem  47928  ovolval4lem1  47932  ovolval4lem2  47933  ovolval5lem2  47936  ovnovollem1  47939  ovnovollem2  47940  vonioolem2  47964  vonicclem2  47967  smflim  48060  nsssmfmbflem  48061  smfmullem4  48077  smfsuplem1  48094  smfsuplem3  48096  smflimsuplem3  48105  fsetsnf  48394  cfsetsnfsetf  48401  cfsetsnfsetfo  48403  imasetpreimafvbijlemf  48756  prproropf1o  48862  fmtnodvds  48902  upgrimwlklem2  49269  isubgr3stgrlem6  49342  linply2cfv  49712  lazssaz  49730  lincvalsc0  49864  lcoc0  49865  linc0scn0  49866  linc1  49868  lincscm  49873  lincresunit3  49924  1arympt1  50081  1arymaptf  50084  2arympt  50092  2arymaptf  50095  ackendofnn0  50127  amgmlemALT  51416