Theorem fmptd 6741

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522   ∈ wcel 2081  ∀wral 3105   ↦ cmpt 5041  ⟶wf 6221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-fv 6233

This theorem is referenced by:  fmpttd  6742  rnmptc  6836  fnwelem  7678  fdiagfn  8303  resixpfo  8348  xpmapenlem  8531  unxpdomlem3  8570  fsuppmptdm  8690  cantnfp1lem1  8987  cantnfp1lem2  8988  cantnfp1lem3  8989  cantnf  9002  updjudhf  9206  fseqenlem2  9297  dfac8clem  9304  coftr  9541  isf34lem2  9641  axcc2lem  9704  axdc2lem  9716  axdc3lem4  9721  pwcfsdom  9851  rpnnen1lem1  12227  caucvg  14869  sumrblem  14901  summolem2a  14905  supcvg  15044  prodrblem  15116  prodmolem2a  15121  crth  15944  eulerthlem1  15947  prmreclem6  16086  4sqlem11  16120  vdwlem2  16147  vdwlem4  16149  vdwlem6  16151  vdwlem10  16155  ramub1lem2  16192  prmgaplcm  16225  frmdup1  17840  grpinvf  17907  cycsubgcl  18059  cycsubgss  18060  conjghm  18130  conjnmz  18133  qusghm  18136  galactghm  18262  symgextf  18276  symgfixf  18295  pmtrdifwrdellem1  18340  odf1  18419  dfod2  18421  pgpssslw  18469  frgpmhm  18618  gsummptfidmsplitres  18771  gsummptfidminv  18787  gsumzunsnd  18796  gsummpt1n0  18805  ablfac1b  18909  ablfac2  18928  abvtrivd  19301  issrngd  19322  pwssplit0  19520  asclf  19799  psr1cl  19870  evlslem1  19982  evlsval2  19987  mulgghm2  20326  isphld  20480  pjff  20538  frlmup1  20624  scmatf  20822  mdetf  20888  maduf  20934  pmatcollpw3fi1lem1  21078  chfacfisf  21146  chfacfisfcpmat  21147  cpmidpmatlem2  21163  lly1stc  21788  txcnmpt  21916  txlm  21940  xkoinjcn  21979  kqffn  22017  txflf  22298  tsmsfbas  22419  ustuqtop0  22532  metdsf  23139  metdsge  23140  mulc1cncf  23196  lebnumlem1  23248  cmetcaulem  23574  ovollb2lem  23772  ovolctb  23774  ovolunlem1a  23780  ovolunlem1  23781  ovoliunlem1  23786  ovoliunlem2  23787  ovoliun  23789  ovolshftlem1  23793  ovolscalem1  23797  ovolicc1  23800  ioombl1lem1  23842  uniioombllem2  23867  volsup2  23889  volcn  23890  vitalilem4  23895  vitalilem5  23896  mbfconst  23917  mbfmax  23933  mbfsup  23948  i1f1lem  23973  i1f1  23974  i1fres  23989  itg1climres  23998  itg2splitlem  24032  itg2split  24033  itg2monolem1  24034  itg2mono  24037  itg2i1fseq  24039  itg2i1fseq2  24040  dvreslem  24190  dvivthlem1  24288  dvfsumrlimf  24305  dvfsumlem3  24308  ftc1lem2  24316  ftc1lem6  24321  tdeglem1  24335  radcnvlem1  24684  pserulm  24693  psercn2  24694  abelthlem4  24705  efif1olem4  24810  lgamgulmlem6  25293  gamcvg  25315  basellem4  25343  basellem7  25346  basellem9  25348  lgsfcl2  25561  lgsqrlem2  25605  lgseisenlem1  25633  dchrmusum2  25752  dchrvmasumiflem1  25759  dchrisum0ff  25765  dchrisum0lem1b  25773  dchrisum0lem2a  25775  abvcxp  25873  padicabv  25888  axlowdimlem15  26425  crctcshwlkn0  27286  wlkiswwlks2lem5  27338  wlkswwlksf1o  27344  wwlksnextfun  27363  clwlkclwwlklem2a  27463  clwlkclwwlkf  27473  clwwlkf  27513  frgrncvvdeqlem4  27773  numclwwlk1lem2f  27826  numclwlk2lem2f  27848  ipblnfi  28323  ubthlem1  28338  htthlem  28385  hlimadd  28661  chscllem1  29105  cnlnadjlem2  29536  strlem3a  29720  hstrlem3a  29728  xppreima2  30085  suppovss  30116  fsuppcurry1  30149  fsuppcurry2  30150  lmodvslmhm  30499  xrge0mulc1cn  30801  esumpcvgval  30954  esumcvg  30962  mbfmco2  31140  eulerpartlems  31235  erdszelem9  32054  cvmlift3lem3  32176  ex-sategoelel  32276  ex-sategoelelomsuc  32281  elmrsubrn  32375  mvhf  32413  iprodefisum  32581  unbdqndv1  33456  knoppf  33483  ftc1anclem3  34500  ftc1anclem5  34502  lflnegcl  35742  lshpkrcl  35783  tendo0cl  37457  frlmsnic  38676  binomcxplemradcnv  40222  binomcxplemcvg  40224  binomcxplemnotnn0  40226  projf1o  40999  mullimc  41439  ellimcabssub0  41440  mullimcf  41446  constlimc  41447  idlimc  41449  neglimc  41470  addlimc  41471  0ellimcdiv  41472  fnlimf  41501  liminfpnfuz  41639  xlimpnfxnegmnf2  41681  cncfshift  41698  icccncfext  41711  cncfiooiccre  41719  fprodsubrecnncnvlem  41732  fprodaddrecnncnvlem  41734  dvmptresicc  41745  ioodvbdlimc1lem1  41757  ioodvbdlimc1lem2  41758  ioodvbdlimc2lem  41760  dvnxpaek  41768  dvnprodlem1  41772  itgsinexplem1  41780  itgiccshift  41806  dirkercncflem2  41931  fourierdlem4  41938  fourierdlem5  41939  fourierdlem9  41943  fourierdlem14  41948  fourierdlem16  41950  fourierdlem17  41951  fourierdlem18  41952  fourierdlem21  41955  fourierdlem22  41956  fourierdlem37  41971  fourierdlem50  41983  fourierdlem51  41984  fourierdlem53  41986  fourierdlem55  41988  fourierdlem57  41990  fourierdlem58  41991  fourierdlem59  41992  fourierdlem60  41993  fourierdlem61  41994  fourierdlem67  42000  fourierdlem68  42001  fourierdlem72  42005  fourierdlem73  42006  fourierdlem74  42007  fourierdlem75  42008  fourierdlem76  42009  fourierdlem78  42011  fourierdlem80  42013  fourierdlem81  42014  fourierdlem83  42016  fourierdlem84  42017  fourierdlem88  42021  fourierdlem92  42025  fourierdlem93  42026  fourierdlem97  42030  fourierdlem101  42034  fourierdlem103  42036  fourierdlem104  42037  fourierdlem111  42044  sqwvfoura  42055  elaa2lem  42060  etransclem1  42062  etransclem8  42069  etransclem20  42081  etransclem33  42094  etransclem35  42096  etransclem39  42100  rrxtopnfi  42114  ioorrnopnxrlem  42133  sge0tsms  42204  sge0snmpt  42207  sge0fsummpt  42214  sge0pr  42218  sge0lessmpt  42223  sge0iunmptlemfi  42237  sge0iunmptlemre  42239  sge0iunmpt  42242  sge0rpcpnf  42245  sge0isum  42251  nnfoctbdjlem  42279  psmeasure  42295  voliunsge0lem  42296  meaiuninclem  42304  meaiuninc3v  42308  meaiininclem  42310  omeiunltfirp  42343  carageniuncllem2  42346  caratheodorylem1  42350  caratheodorylem2  42351  isomenndlem  42354  hoicvr  42372  hoicvrrex  42380  ovnsupge0  42381  ovnlecvr  42382  ovnf  42387  ovn0lem  42389  ovnsubaddlem1  42394  ovnsubadd  42396  hsphoif  42400  sge0hsphoire  42413  hoidmv1lelem1  42415  hoidmv1lelem2  42416  hoidmv1lelem3  42417  hoidmv1le  42418  hoidmvlelem2  42420  hoidmvlelem3  42421  ovnhoilem1  42425  ovnsubadd2lem  42469  ovolval4lem1  42473  ovolval4lem2  42474  ovolval5lem2  42477  ovnovollem1  42480  ovnovollem2  42481  vonioolem2  42505  vonicclem2  42508  smfmbfcex  42578  smflim  42595  nsssmfmbflem  42596  smfmullem4  42611  smfsuplem1  42627  smfsuplem3  42629  smflimsuplem3  42638  prproropf1o  43151  fmtnodvds  43188  c0mgm  43658  c0mhm  43659  c0snmgmhm  43663  lincvalsc0  43956  lcoc0  43957  linc0scn0  43958  linc1  43960  lincscm  43965  lincresunit3  44016  amgmlemALT  44384