Theorem fmptd 7048

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1541   ∈ wcel 2106  ∀wral 3062   ↦ cmpt 5179  ⟶wf 6479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5247  ax-nul 5254  ax-pr 5376

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-sn 4578  df-pr 4580  df-op 4584  df-br 5097  df-opab 5159  df-mpt 5180  df-id 5522  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6485  df-fn 6486  df-f 6487

This theorem is referenced by:  fmpttd  7049  rnmptcOLD  7143  fnwelem  8043  fsetfcdm  8723  fsetfocdm  8724  fdiagfn  8753  resixpfo  8799  xpmapenlem  9013  unxpdomlem3  9121  fsuppmptdm  9241  cantnfp1lem1  9539  cantnfp1lem2  9540  cantnfp1lem3  9541  cantnf  9554  updjudhf  9792  fseqenlem2  9886  dfac8clem  9893  coftr  10134  isf34lem2  10234  axcc2lem  10297  axdc2lem  10309  axdc3lem4  10314  pwcfsdom  10444  rpnnen1lem1  12823  caucvg  15489  sumrblem  15522  summolem2a  15526  supcvg  15667  prodrblem  15738  prodmolem2a  15743  crth  16576  eulerthlem1  16579  prmreclem6  16719  4sqlem11  16753  vdwlem2  16780  vdwlem4  16782  vdwlem6  16784  vdwlem10  16788  ramub1lem2  16825  prmgaplcm  16858  frmdup1  18599  grpinvf  18722  mulgnngsum  18805  cycsubm  18917  cycsubgcl  18921  cycsubgss  18922  conjghm  18961  conjnmz  18964  qusghm  18967  galactghm  19108  symgextf  19121  symgfixf  19140  pmtrdifwrdellem1  19185  odf1  19265  dfod2  19267  pgpssslw  19315  frgpmhm  19466  gsummptfidmsplitres  19626  gsummptfidminv  19642  gsumzunsnd  19651  gsummpt1n0  19660  ablfac1b  19767  ablfac2  19786  abvtrivd  20205  issrngd  20226  pwssplit0  20425  mulgghm2  20803  isphld  20964  pjff  21024  frlmup1  21110  asclf  21191  psr1cl  21276  evlslem1  21397  evlsval2  21402  scmatf  21783  mdetf  21849  maduf  21895  pmatcollpw3fi1lem1  22040  chfacfisf  22108  chfacfisfcpmat  22109  cpmidpmatlem2  22125  lly1stc  22752  txcnmpt  22880  txlm  22904  xkoinjcn  22943  kqffn  22981  txflf  23262  tsmsfbas  23384  ustuqtop0  23497  metdsf  24116  metdsge  24117  mulc1cncf  24173  lebnumlem1  24229  cmetcaulem  24557  ovollb2lem  24757  ovolctb  24759  ovolunlem1a  24765  ovolunlem1  24766  ovoliunlem1  24771  ovoliunlem2  24772  ovoliun  24774  ovolshftlem1  24778  ovolscalem1  24782  ovolicc1  24785  ioombl1lem1  24827  uniioombllem2  24852  volsup2  24874  volcn  24875  vitalilem4  24880  vitalilem5  24881  mbfconst  24902  mbfmax  24918  mbfsup  24933  i1f1lem  24958  i1f1  24959  i1fres  24975  itg1climres  24984  itg2splitlem  25018  itg2split  25019  itg2monolem1  25020  itg2mono  25023  itg2i1fseq  25025  itg2i1fseq2  25026  dvreslem  25178  dvmptresicc  25185  dvivthlem1  25277  dvfsumrlimf  25294  dvfsumlem3  25297  ftc1lem2  25305  ftc1lem6  25310  tdeglem1OLD  25326  radcnvlem1  25677  pserulm  25686  psercn2  25687  abelthlem4  25698  efif1olem4  25806  lgamgulmlem6  26288  gamcvg  26310  basellem4  26338  basellem7  26341  basellem9  26343  lgsfcl2  26556  lgsqrlem2  26600  lgseisenlem1  26628  dchrmusum2  26747  dchrvmasumiflem1  26754  dchrisum0ff  26760  dchrisum0lem1b  26768  dchrisum0lem2a  26770  abvcxp  26868  padicabv  26883  axlowdimlem15  27612  crctcshwlkn0  28473  wlkiswwlks2lem5  28525  wlkswwlksf1o  28531  wwlksnextfun  28550  clwlkclwwlklem2a  28649  clwlkclwwlkf  28659  clwwlkf  28698  frgrncvvdeqlem4  28953  numclwwlk1lem2f  29006  numclwlk2lem2f  29028  ipblnfi  29504  ubthlem1  29519  htthlem  29566  hlimadd  29842  chscllem1  30286  cnlnadjlem2  30717  strlem3a  30901  hstrlem3a  30909  xppreima2  31273  suppovss  31302  fsuppcurry1  31345  fsuppcurry2  31346  pwrssmgc  31563  lmodvslmhm  31595  frobrhm  31770  nsgmgc  31892  elrspunidl  31901  rhmpreimacnlem  32130  rhmpreimacn  32131  xrge0mulc1cn  32187  esumpcvgval  32342  esumcvg  32350  mbfmco2  32530  eulerpartlems  32625  erdszelem9  33458  cvmlift3lem3  33580  ex-sategoelel  33680  ex-sategoelelomsuc  33685  elmrsubrn  33779  mvhf  33817  iprodefisum  33997  unbdqndv1  34825  knoppf  34852  ftc1anclem3  36008  ftc1anclem5  36010  lflnegcl  37393  lshpkrcl  37434  tendo0cl  39109  aks6d1c2p1  40404  sticksstones2  40411  sticksstones8  40417  sticksstones9  40418  sticksstones10  40419  sticksstones11  40420  sticksstones12a  40421  sticksstones17  40427  sticksstones18  40428  metakunt1  40433  metakunt2  40434  metakunt19  40451  metakunt25  40457  selvval2lem5  40534  frlmsnic  40574  evlsval3  40583  evlsbagval  40586  binomcxplemradcnv  42343  binomcxplemcvg  42345  binomcxplemnotnn0  42347  projf1o  43115  mullimc  43545  ellimcabssub0  43546  mullimcf  43552  constlimc  43553  idlimc  43555  neglimc  43576  addlimc  43577  0ellimcdiv  43578  fnlimf  43607  liminfpnfuz  43745  xlimpnfxnegmnf2  43787  cncfshift  43803  icccncfext  43816  cncfiooiccre  43824  fprodsubrecnncnvlem  43836  fprodaddrecnncnvlem  43838  ioodvbdlimc1lem1  43860  ioodvbdlimc1lem2  43861  ioodvbdlimc2lem  43863  dvnxpaek  43871  dvnprodlem1  43875  itgsinexplem1  43883  itgiccshift  43909  dirkercncflem2  44033  fourierdlem4  44040  fourierdlem5  44041  fourierdlem9  44045  fourierdlem14  44050  fourierdlem16  44052  fourierdlem17  44053  fourierdlem18  44054  fourierdlem21  44057  fourierdlem22  44058  fourierdlem37  44073  fourierdlem50  44085  fourierdlem51  44086  fourierdlem53  44088  fourierdlem55  44090  fourierdlem57  44092  fourierdlem58  44093  fourierdlem59  44094  fourierdlem60  44095  fourierdlem61  44096  fourierdlem67  44102  fourierdlem68  44103  fourierdlem72  44107  fourierdlem73  44108  fourierdlem74  44109  fourierdlem75  44110  fourierdlem76  44111  fourierdlem78  44113  fourierdlem80  44115  fourierdlem81  44116  fourierdlem83  44118  fourierdlem84  44119  fourierdlem88  44123  fourierdlem92  44127  fourierdlem93  44128  fourierdlem97  44132  fourierdlem101  44136  fourierdlem103  44138  fourierdlem104  44139  fourierdlem111  44146  sqwvfoura  44157  elaa2lem  44162  etransclem1  44164  etransclem8  44171  etransclem20  44183  etransclem33  44196  etransclem35  44198  etransclem39  44202  rrxtopnfi  44216  ioorrnopnxrlem  44235  sge0tsms  44307  sge0snmpt  44310  sge0fsummpt  44317  sge0pr  44321  sge0lessmpt  44326  sge0iunmptlemfi  44340  sge0iunmptlemre  44342  sge0iunmpt  44345  sge0rpcpnf  44348  sge0isum  44354  nnfoctbdjlem  44382  psmeasure  44398  voliunsge0lem  44399  meaiuninclem  44407  meaiuninc3v  44411  meaiininclem  44413  omeiunltfirp  44446  carageniuncllem2  44449  caratheodorylem1  44453  caratheodorylem2  44454  isomenndlem  44457  hoicvr  44475  hoicvrrex  44483  ovnsupge0  44484  ovnlecvr  44485  ovnf  44490  ovn0lem  44492  ovnsubaddlem1  44497  ovnsubadd  44499  hsphoif  44503  sge0hsphoire  44516  hoidmv1lelem1  44518  hoidmv1lelem2  44519  hoidmv1lelem3  44520  hoidmv1le  44521  hoidmvlelem2  44523  hoidmvlelem3  44524  ovnhoilem1  44528  ovnsubadd2lem  44572  ovolval4lem1  44576  ovolval4lem2  44577  ovolval5lem2  44580  ovnovollem1  44583  ovnovollem2  44584  vonioolem2  44608  vonicclem2  44611  smflim  44704  nsssmfmbflem  44705  smfmullem4  44721  smfsuplem1  44738  smfsuplem3  44740  smflimsuplem3  44749  fsetsnf  44963  cfsetsnfsetf  44970  cfsetsnfsetfo  44972  imasetpreimafvbijlemf  45271  prproropf1o  45377  fmtnodvds  45414  c0mgm  45885  c0mhm  45886  c0snmgmhm  45890  lincvalsc0  46180  lcoc0  46181  linc0scn0  46182  linc1  46184  lincscm  46189  lincresunit3  46240  1arympt1  46402  1arymaptf  46405  2arympt  46413  2arymaptf  46416  ackendofnn0  46448  amgmlemALT  46925