Theorem fmptd 6881

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1536   ∈ wcel 2113  ∀wral 3141   ↦ cmpt 5149  ⟶wf 6354

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pr 5333

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-fv 6366

This theorem is referenced by:  fmpttd  6882  rnmptcOLD  6973  fnwelem  7828  fdiagfn  8457  resixpfo  8503  xpmapenlem  8687  unxpdomlem3  8727  fsuppmptdm  8847  cantnfp1lem1  9144  cantnfp1lem2  9145  cantnfp1lem3  9146  cantnf  9159  updjudhf  9363  fseqenlem2  9454  dfac8clem  9461  coftr  9698  isf34lem2  9798  axcc2lem  9861  axdc2lem  9873  axdc3lem4  9878  pwcfsdom  10008  rpnnen1lem1  12380  caucvg  15038  sumrblem  15071  summolem2a  15075  supcvg  15214  prodrblem  15286  prodmolem2a  15291  crth  16118  eulerthlem1  16121  prmreclem6  16260  4sqlem11  16294  vdwlem2  16321  vdwlem4  16323  vdwlem6  16325  vdwlem10  16329  ramub1lem2  16366  prmgaplcm  16399  frmdup1  18032  grpinvf  18153  mulgnngsum  18236  cycsubm  18348  cycsubgcl  18352  cycsubgss  18353  conjghm  18392  conjnmz  18395  qusghm  18398  galactghm  18535  symgextf  18548  symgfixf  18567  pmtrdifwrdellem1  18612  odf1  18692  dfod2  18694  pgpssslw  18742  frgpmhm  18894  gsummptfidmsplitres  19054  gsummptfidminv  19070  gsumzunsnd  19079  gsummpt1n0  19088  ablfac1b  19195  ablfac2  19214  abvtrivd  19614  issrngd  19635  pwssplit0  19833  asclf  20114  psr1cl  20185  evlslem1  20298  evlsval2  20303  mulgghm2  20647  isphld  20801  pjff  20859  frlmup1  20945  scmatf  21141  mdetf  21207  maduf  21253  pmatcollpw3fi1lem1  21397  chfacfisf  21465  chfacfisfcpmat  21466  cpmidpmatlem2  21482  lly1stc  22107  txcnmpt  22235  txlm  22259  xkoinjcn  22298  kqffn  22336  txflf  22617  tsmsfbas  22739  ustuqtop0  22852  metdsf  23459  metdsge  23460  mulc1cncf  23516  lebnumlem1  23568  cmetcaulem  23894  ovollb2lem  24092  ovolctb  24094  ovolunlem1a  24100  ovolunlem1  24101  ovoliunlem1  24106  ovoliunlem2  24107  ovoliun  24109  ovolshftlem1  24113  ovolscalem1  24117  ovolicc1  24120  ioombl1lem1  24162  uniioombllem2  24187  volsup2  24209  volcn  24210  vitalilem4  24215  vitalilem5  24216  mbfconst  24237  mbfmax  24253  mbfsup  24268  i1f1lem  24293  i1f1  24294  i1fres  24309  itg1climres  24318  itg2splitlem  24352  itg2split  24353  itg2monolem1  24354  itg2mono  24357  itg2i1fseq  24359  itg2i1fseq2  24360  dvreslem  24510  dvivthlem1  24608  dvfsumrlimf  24625  dvfsumlem3  24628  ftc1lem2  24636  ftc1lem6  24641  tdeglem1  24655  radcnvlem1  25004  pserulm  25013  psercn2  25014  abelthlem4  25025  efif1olem4  25132  lgamgulmlem6  25614  gamcvg  25636  basellem4  25664  basellem7  25667  basellem9  25669  lgsfcl2  25882  lgsqrlem2  25926  lgseisenlem1  25954  dchrmusum2  26073  dchrvmasumiflem1  26080  dchrisum0ff  26086  dchrisum0lem1b  26094  dchrisum0lem2a  26096  abvcxp  26194  padicabv  26209  axlowdimlem15  26745  crctcshwlkn0  27602  wlkiswwlks2lem5  27654  wlkswwlksf1o  27660  wwlksnextfun  27679  clwlkclwwlklem2a  27779  clwlkclwwlkf  27789  clwwlkf  27829  frgrncvvdeqlem4  28084  numclwwlk1lem2f  28137  numclwlk2lem2f  28159  ipblnfi  28635  ubthlem1  28650  htthlem  28697  hlimadd  28973  chscllem1  29417  cnlnadjlem2  29848  strlem3a  30032  hstrlem3a  30040  xppreima2  30398  suppovss  30429  fsuppcurry1  30464  fsuppcurry2  30465  lmodvslmhm  30692  xrge0mulc1cn  31188  esumpcvgval  31341  esumcvg  31349  mbfmco2  31527  eulerpartlems  31622  erdszelem9  32450  cvmlift3lem3  32572  ex-sategoelel  32672  ex-sategoelelomsuc  32677  elmrsubrn  32771  mvhf  32809  iprodefisum  32977  unbdqndv1  33851  knoppf  33878  ftc1anclem3  34973  ftc1anclem5  34975  lflnegcl  36215  lshpkrcl  36256  tendo0cl  37930  selvval2lem5  39143  frlmsnic  39155  binomcxplemradcnv  40690  binomcxplemcvg  40692  binomcxplemnotnn0  40694  projf1o  41465  mullimc  41903  ellimcabssub0  41904  mullimcf  41910  constlimc  41911  idlimc  41913  neglimc  41934  addlimc  41935  0ellimcdiv  41936  fnlimf  41965  liminfpnfuz  42103  xlimpnfxnegmnf2  42145  cncfshift  42163  icccncfext  42176  cncfiooiccre  42184  fprodsubrecnncnvlem  42197  fprodaddrecnncnvlem  42199  dvmptresicc  42210  ioodvbdlimc1lem1  42222  ioodvbdlimc1lem2  42223  ioodvbdlimc2lem  42225  dvnxpaek  42233  dvnprodlem1  42237  itgsinexplem1  42245  itgiccshift  42271  dirkercncflem2  42396  fourierdlem4  42403  fourierdlem5  42404  fourierdlem9  42408  fourierdlem14  42413  fourierdlem16  42415  fourierdlem17  42416  fourierdlem18  42417  fourierdlem21  42420  fourierdlem22  42421  fourierdlem37  42436  fourierdlem50  42448  fourierdlem51  42449  fourierdlem53  42451  fourierdlem55  42453  fourierdlem57  42455  fourierdlem58  42456  fourierdlem59  42457  fourierdlem60  42458  fourierdlem61  42459  fourierdlem67  42465  fourierdlem68  42466  fourierdlem72  42470  fourierdlem73  42471  fourierdlem74  42472  fourierdlem75  42473  fourierdlem76  42474  fourierdlem78  42476  fourierdlem80  42478  fourierdlem81  42479  fourierdlem83  42481  fourierdlem84  42482  fourierdlem88  42486  fourierdlem92  42490  fourierdlem93  42491  fourierdlem97  42495  fourierdlem101  42499  fourierdlem103  42501  fourierdlem104  42502  fourierdlem111  42509  sqwvfoura  42520  elaa2lem  42525  etransclem1  42527  etransclem8  42534  etransclem20  42546  etransclem33  42559  etransclem35  42561  etransclem39  42565  rrxtopnfi  42579  ioorrnopnxrlem  42598  sge0tsms  42669  sge0snmpt  42672  sge0fsummpt  42679  sge0pr  42683  sge0lessmpt  42688  sge0iunmptlemfi  42702  sge0iunmptlemre  42704  sge0iunmpt  42707  sge0rpcpnf  42710  sge0isum  42716  nnfoctbdjlem  42744  psmeasure  42760  voliunsge0lem  42761  meaiuninclem  42769  meaiuninc3v  42773  meaiininclem  42775  omeiunltfirp  42808  carageniuncllem2  42811  caratheodorylem1  42815  caratheodorylem2  42816  isomenndlem  42819  hoicvr  42837  hoicvrrex  42845  ovnsupge0  42846  ovnlecvr  42847  ovnf  42852  ovn0lem  42854  ovnsubaddlem1  42859  ovnsubadd  42861  hsphoif  42865  sge0hsphoire  42878  hoidmv1lelem1  42880  hoidmv1lelem2  42881  hoidmv1lelem3  42882  hoidmv1le  42883  hoidmvlelem2  42885  hoidmvlelem3  42886  ovnhoilem1  42890  ovnsubadd2lem  42934  ovolval4lem1  42938  ovolval4lem2  42939  ovolval5lem2  42942  ovnovollem1  42945  ovnovollem2  42946  vonioolem2  42970  vonicclem2  42973  smfmbfcex  43043  smflim  43060  nsssmfmbflem  43061  smfmullem4  43076  smfsuplem1  43092  smfsuplem3  43094  smflimsuplem3  43103  imasetpreimafvbijlemf  43568  prproropf1o  43676  fmtnodvds  43713  c0mgm  44187  c0mhm  44188  c0snmgmhm  44192  lincvalsc0  44483  lcoc0  44484  linc0scn0  44485  linc1  44487  lincscm  44492  lincresunit3  44543  amgmlemALT  44911