Theorem fmptd 6878

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3138   ↦ cmpt 5146  ⟶wf 6351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363

This theorem is referenced by:  fmpttd  6879  rnmptcOLD  6970  fnwelem  7825  fdiagfn  8454  resixpfo  8500  xpmapenlem  8684  unxpdomlem3  8724  fsuppmptdm  8844  cantnfp1lem1  9141  cantnfp1lem2  9142  cantnfp1lem3  9143  cantnf  9156  updjudhf  9360  fseqenlem2  9451  dfac8clem  9458  coftr  9695  isf34lem2  9795  axcc2lem  9858  axdc2lem  9870  axdc3lem4  9875  pwcfsdom  10005  rpnnen1lem1  12378  caucvg  15035  sumrblem  15068  summolem2a  15072  supcvg  15211  prodrblem  15283  prodmolem2a  15288  crth  16115  eulerthlem1  16118  prmreclem6  16257  4sqlem11  16291  vdwlem2  16318  vdwlem4  16320  vdwlem6  16322  vdwlem10  16326  ramub1lem2  16363  prmgaplcm  16396  frmdup1  18029  grpinvf  18150  mulgnngsum  18233  cycsubm  18345  cycsubgcl  18349  cycsubgss  18350  conjghm  18389  conjnmz  18392  qusghm  18395  galactghm  18532  symgextf  18545  symgfixf  18564  pmtrdifwrdellem1  18609  odf1  18689  dfod2  18691  pgpssslw  18739  frgpmhm  18891  gsummptfidmsplitres  19051  gsummptfidminv  19067  gsumzunsnd  19076  gsummpt1n0  19085  ablfac1b  19192  ablfac2  19211  abvtrivd  19611  issrngd  19632  pwssplit0  19830  asclf  20111  psr1cl  20182  evlslem1  20295  evlsval2  20300  mulgghm2  20644  isphld  20798  pjff  20856  frlmup1  20942  scmatf  21138  mdetf  21204  maduf  21250  pmatcollpw3fi1lem1  21394  chfacfisf  21462  chfacfisfcpmat  21463  cpmidpmatlem2  21479  lly1stc  22104  txcnmpt  22232  txlm  22256  xkoinjcn  22295  kqffn  22333  txflf  22614  tsmsfbas  22736  ustuqtop0  22849  metdsf  23456  metdsge  23457  mulc1cncf  23513  lebnumlem1  23565  cmetcaulem  23891  ovollb2lem  24089  ovolctb  24091  ovolunlem1a  24097  ovolunlem1  24098  ovoliunlem1  24103  ovoliunlem2  24104  ovoliun  24106  ovolshftlem1  24110  ovolscalem1  24114  ovolicc1  24117  ioombl1lem1  24159  uniioombllem2  24184  volsup2  24206  volcn  24207  vitalilem4  24212  vitalilem5  24213  mbfconst  24234  mbfmax  24250  mbfsup  24265  i1f1lem  24290  i1f1  24291  i1fres  24306  itg1climres  24315  itg2splitlem  24349  itg2split  24350  itg2monolem1  24351  itg2mono  24354  itg2i1fseq  24356  itg2i1fseq2  24357  dvreslem  24507  dvivthlem1  24605  dvfsumrlimf  24622  dvfsumlem3  24625  ftc1lem2  24633  ftc1lem6  24638  tdeglem1  24652  radcnvlem1  25001  pserulm  25010  psercn2  25011  abelthlem4  25022  efif1olem4  25129  lgamgulmlem6  25611  gamcvg  25633  basellem4  25661  basellem7  25664  basellem9  25666  lgsfcl2  25879  lgsqrlem2  25923  lgseisenlem1  25951  dchrmusum2  26070  dchrvmasumiflem1  26077  dchrisum0ff  26083  dchrisum0lem1b  26091  dchrisum0lem2a  26093  abvcxp  26191  padicabv  26206  axlowdimlem15  26742  crctcshwlkn0  27599  wlkiswwlks2lem5  27651  wlkswwlksf1o  27657  wwlksnextfun  27676  clwlkclwwlklem2a  27776  clwlkclwwlkf  27786  clwwlkf  27826  frgrncvvdeqlem4  28081  numclwwlk1lem2f  28134  numclwlk2lem2f  28156  ipblnfi  28632  ubthlem1  28647  htthlem  28694  hlimadd  28970  chscllem1  29414  cnlnadjlem2  29845  strlem3a  30029  hstrlem3a  30037  xppreima2  30395  suppovss  30426  fsuppcurry1  30461  fsuppcurry2  30462  lmodvslmhm  30688  xrge0mulc1cn  31184  esumpcvgval  31337  esumcvg  31345  mbfmco2  31523  eulerpartlems  31618  erdszelem9  32446  cvmlift3lem3  32568  ex-sategoelel  32668  ex-sategoelelomsuc  32673  elmrsubrn  32767  mvhf  32805  iprodefisum  32973  unbdqndv1  33847  knoppf  33874  ftc1anclem3  34984  ftc1anclem5  34986  lflnegcl  36226  lshpkrcl  36267  tendo0cl  37941  selvval2lem5  39186  frlmsnic  39198  binomcxplemradcnv  40733  binomcxplemcvg  40735  binomcxplemnotnn0  40737  projf1o  41508  mullimc  41946  ellimcabssub0  41947  mullimcf  41953  constlimc  41954  idlimc  41956  neglimc  41977  addlimc  41978  0ellimcdiv  41979  fnlimf  42008  liminfpnfuz  42146  xlimpnfxnegmnf2  42188  cncfshift  42206  icccncfext  42219  cncfiooiccre  42227  fprodsubrecnncnvlem  42240  fprodaddrecnncnvlem  42242  dvmptresicc  42253  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnxpaek  42276  dvnprodlem1  42280  itgsinexplem1  42288  itgiccshift  42314  dirkercncflem2  42438  fourierdlem4  42445  fourierdlem5  42446  fourierdlem9  42450  fourierdlem14  42455  fourierdlem16  42457  fourierdlem17  42458  fourierdlem18  42459  fourierdlem21  42462  fourierdlem22  42463  fourierdlem37  42478  fourierdlem50  42490  fourierdlem51  42491  fourierdlem53  42493  fourierdlem55  42495  fourierdlem57  42497  fourierdlem58  42498  fourierdlem59  42499  fourierdlem60  42500  fourierdlem61  42501  fourierdlem67  42507  fourierdlem68  42508  fourierdlem72  42512  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem78  42518  fourierdlem80  42520  fourierdlem81  42521  fourierdlem83  42523  fourierdlem84  42524  fourierdlem88  42528  fourierdlem92  42532  fourierdlem93  42533  fourierdlem97  42537  fourierdlem101  42541  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  sqwvfoura  42562  elaa2lem  42567  etransclem1  42569  etransclem8  42576  etransclem20  42588  etransclem33  42601  etransclem35  42603  etransclem39  42607  rrxtopnfi  42621  ioorrnopnxrlem  42640  sge0tsms  42711  sge0snmpt  42714  sge0fsummpt  42721  sge0pr  42725  sge0lessmpt  42730  sge0iunmptlemfi  42744  sge0iunmptlemre  42746  sge0iunmpt  42749  sge0rpcpnf  42752  sge0isum  42758  nnfoctbdjlem  42786  psmeasure  42802  voliunsge0lem  42803  meaiuninclem  42811  meaiuninc3v  42815  meaiininclem  42817  omeiunltfirp  42850  carageniuncllem2  42853  caratheodorylem1  42857  caratheodorylem2  42858  isomenndlem  42861  hoicvr  42879  hoicvrrex  42887  ovnsupge0  42888  ovnlecvr  42889  ovnf  42894  ovn0lem  42896  ovnsubaddlem1  42901  ovnsubadd  42903  hsphoif  42907  sge0hsphoire  42920  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmv1le  42925  hoidmvlelem2  42927  hoidmvlelem3  42928  ovnhoilem1  42932  ovnsubadd2lem  42976  ovolval4lem1  42980  ovolval4lem2  42981  ovolval5lem2  42984  ovnovollem1  42987  ovnovollem2  42988  vonioolem2  43012  vonicclem2  43015  smfmbfcex  43085  smflim  43102  nsssmfmbflem  43103  smfmullem4  43118  smfsuplem1  43134  smfsuplem3  43136  smflimsuplem3  43145  imasetpreimafvbijlemf  43610  prproropf1o  43718  fmtnodvds  43755  c0mgm  44229  c0mhm  44230  c0snmgmhm  44234  lincvalsc0  44525  lcoc0  44526  linc0scn0  44527  linc1  44529  lincscm  44534  lincresunit3  44585  amgmlemALT  44953