Theorem fmptd 7058

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052   ↦ cmpt 5167  ⟶wf 6486

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-fun 6492  df-fn 6493  df-f 6494

This theorem is referenced by:  fmpttd  7059  fnwelem  8072  fsetfcdm  8798  fdiagfn  8829  resixpfo  8875  xpmapenlem  9073  unxpdomlem3  9159  fsuppmptdm  9280  cantnfp1lem1  9588  cantnfp1lem2  9589  cantnfp1lem3  9590  cantnf  9603  updjudhf  9844  fseqenlem2  9936  dfac8clem  9943  coftr  10184  isf34lem2  10284  axcc2lem  10347  axdc2lem  10359  axdc3lem4  10364  pwcfsdom  10495  rpnnen1lem1  12892  tpf  14423  caucvg  15603  sumrblem  15635  summolem2a  15639  supcvg  15780  prodrblem  15853  prodmolem2a  15858  crth  16706  eulerthlem1  16709  prmreclem6  16850  4sqlem11  16884  vdwlem2  16911  vdwlem4  16913  vdwlem6  16915  vdwlem10  16919  ramub1lem2  16956  prmgaplcm  16989  frmdup1  18790  grpinvf  18920  mulgnngsum  19013  cycsubm  19135  cycsubgcl  19139  cycsubgss  19140  conjghm  19182  conjnmz  19185  qusghm  19188  galactghm  19337  symgextf  19350  symgfixf  19369  pmtrdifwrdellem1  19414  odf1  19495  dfod2  19497  pgpssslw  19547  frgpmhm  19698  gsummptfidmsplitres  19864  gsummptfidminv  19880  gsumzunsnd  19889  gsummpt1n0  19898  ablfac1b  20005  ablfac2  20024  c0mgm  20397  c0mhm  20398  c0snmgmhm  20400  abvtrivd  20767  issrngd  20790  pwssplit0  21012  rngqiprngimf  21254  mulgghm2  21433  frobrhm  21532  isphld  21611  pjff  21669  frlmup1  21755  asclf  21838  psr1cl  21917  evlslem1  22038  evlsval2  22043  evlsval3  22045  evls1maprhm  22319  rhmmpl  22326  scmatf  22472  mdetf  22538  maduf  22584  pmatcollpw3fi1lem1  22729  chfacfisf  22797  chfacfisfcpmat  22798  cpmidpmatlem2  22814  lly1stc  23439  txcnmpt  23567  txlm  23591  xkoinjcn  23630  kqffn  23668  txflf  23949  tsmsfbas  24071  ustuqtop0  24183  metdsf  24792  metdsge  24793  mulc1cncf  24850  lebnumlem1  24906  cmetcaulem  25233  ovollb2lem  25433  ovolctb  25435  ovolunlem1a  25441  ovolunlem1  25442  ovoliunlem1  25447  ovoliunlem2  25448  ovoliun  25450  ovolshftlem1  25454  ovolscalem1  25458  ovolicc1  25461  ioombl1lem1  25503  uniioombllem2  25528  volsup2  25550  volcn  25551  vitalilem4  25556  vitalilem5  25557  mbfconst  25578  mbfmax  25594  mbfsup  25609  i1f1lem  25634  i1f1  25635  i1fres  25650  itg1climres  25659  itg2splitlem  25693  itg2split  25694  itg2monolem1  25695  itg2mono  25698  itg2i1fseq  25700  itg2i1fseq2  25701  dvreslem  25854  dvmptresicc  25861  dvivthlem1  25954  dvfsumrlimf  25972  dvfsumlem3  25976  ftc1lem2  25984  ftc1lem6  25989  radcnvlem1  26362  pserulm  26371  psercn2  26372  psercn2OLD  26373  abelthlem4  26384  efif1olem4  26494  lgamgulmlem6  26984  gamcvg  27006  basellem4  27034  basellem7  27037  basellem9  27039  lgsfcl2  27254  lgsqrlem2  27298  lgseisenlem1  27326  dchrmusum2  27445  dchrvmasumiflem1  27452  dchrisum0ff  27458  dchrisum0lem1b  27466  dchrisum0lem2a  27468  abvcxp  27566  padicabv  27581  axlowdimlem15  29013  crctcshwlkn0  29878  wlkiswwlks2lem5  29930  wlkswwlksf1o  29936  wwlksnextfun  29955  clwlkclwwlklem2a  30057  clwlkclwwlkf  30067  clwwlkf  30106  frgrncvvdeqlem4  30361  numclwwlk1lem2f  30414  numclwlk2lem2f  30436  ipblnfi  30915  ubthlem1  30930  htthlem  30977  hlimadd  31253  chscllem1  31697  cnlnadjlem2  32128  strlem3a  32312  hstrlem3a  32320  xppreima2  32713  suppovss  32743  fsuppcurry1  32786  fsuppcurry2  32787  pwrssmgc  33065  mndlactf1  33091  mndlactfo  33092  mndractf1  33093  mndractfo  33094  lmodvslmhm  33116  conjga  33236  rlocf1  33339  nsgmgc  33477  elrspunidl  33493  r1plmhm  33675  r1pquslmic  33676  mplvrpmga  33694  mplvrpmmhm  33695  mplvrpmrhm  33696  psrmonprod  33701  mplmonprod  33703  ply1degltdimlem  33772  ply1degltdim  33773  extdgfialglem1  33842  algextdeglem8  33874  rhmpreimacnlem  34034  rhmpreimacn  34035  xrge0mulc1cn  34091  esumpcvgval  34228  esumcvg  34236  mbfmco2  34415  eulerpartlems  34510  erdszelem9  35387  cvmlift3lem3  35509  ex-sategoelel  35609  ex-sategoelelomsuc  35614  elmrsubrn  35708  mvhf  35746  iprodefisum  35929  unbdqndv1  36766  knoppf  36793  ftc1anclem3  38007  ftc1anclem5  38009  lflnegcl  39512  lshpkrcl  39553  tendo0cl  41227  primrootscoprf  42532  aks6d1c2p1  42549  aks6d1c4  42555  aks6d1c2lem4  42558  aks6d1c2  42561  aks6d1c5lem0  42566  aks6d1c5  42570  sticksstones2  42578  sticksstones8  42584  sticksstones9  42585  sticksstones10  42586  sticksstones11  42587  sticksstones12a  42588  sticksstones17  42594  sticksstones18  42595  aks6d1c6lem2  42602  aks6d1c6lem3  42603  aks6d1c6lem4  42604  aks6d1c6isolem1  42605  aks6d1c6isolem2  42606  aks6d1c6isolem3  42607  aks6d1c6lem5  42608  aks5lem2  42618  frlmsnic  42984  rhmpsr  42994  mplmapghm  42996  evlsbagval  43001  evlsmaprhm  43005  selvcllem5  43014  cantnfub  43752  binomcxplemradcnv  44782  binomcxplemcvg  44784  binomcxplemnotnn0  44786  projf1o  45629  mullimc  46050  ellimcabssub0  46051  mullimcf  46057  constlimc  46058  idlimc  46060  neglimc  46079  addlimc  46080  0ellimcdiv  46081  fnlimf  46110  liminfpnfuz  46248  xlimpnfxnegmnf2  46290  cncfshift  46306  icccncfext  46319  cncfiooiccre  46327  fprodsubrecnncnvlem  46339  fprodaddrecnncnvlem  46341  ioodvbdlimc1lem1  46363  ioodvbdlimc1lem2  46364  ioodvbdlimc2lem  46366  dvnxpaek  46374  dvnprodlem1  46378  itgsinexplem1  46386  itgiccshift  46412  dirkercncflem2  46536  fourierdlem4  46543  fourierdlem5  46544  fourierdlem9  46548  fourierdlem14  46553  fourierdlem16  46555  fourierdlem17  46556  fourierdlem18  46557  fourierdlem21  46560  fourierdlem22  46561  fourierdlem37  46576  fourierdlem50  46588  fourierdlem51  46589  fourierdlem53  46591  fourierdlem55  46593  fourierdlem57  46595  fourierdlem58  46596  fourierdlem59  46597  fourierdlem60  46598  fourierdlem61  46599  fourierdlem67  46605  fourierdlem68  46606  fourierdlem72  46610  fourierdlem73  46611  fourierdlem74  46612  fourierdlem75  46613  fourierdlem76  46614  fourierdlem78  46616  fourierdlem80  46618  fourierdlem81  46619  fourierdlem83  46621  fourierdlem84  46622  fourierdlem88  46626  fourierdlem92  46630  fourierdlem93  46631  fourierdlem97  46635  fourierdlem101  46639  fourierdlem103  46641  fourierdlem104  46642  fourierdlem111  46649  sqwvfoura  46660  elaa2lem  46665  etransclem1  46667  etransclem8  46674  etransclem20  46686  etransclem33  46699  etransclem35  46701  etransclem39  46705  rrxtopnfi  46719  ioorrnopnxrlem  46738  sge0tsms  46812  sge0snmpt  46815  sge0fsummpt  46822  sge0pr  46826  sge0lessmpt  46831  sge0iunmptlemfi  46845  sge0iunmptlemre  46847  sge0iunmpt  46850  sge0rpcpnf  46853  sge0isum  46859  nnfoctbdjlem  46887  psmeasure  46903  voliunsge0lem  46904  meaiuninclem  46912  meaiuninc3v  46916  meaiininclem  46918  omeiunltfirp  46951  carageniuncllem2  46954  caratheodorylem1  46958  caratheodorylem2  46959  isomenndlem  46962  hoicvrrex  46988  ovnsupge0  46989  ovnlecvr  46990  ovnf  46995  ovn0lem  46997  ovnsubaddlem1  47002  ovnsubadd  47004  hsphoif  47008  sge0hsphoire  47021  hoidmv1lelem1  47023  hoidmv1lelem2  47024  hoidmv1lelem3  47025  hoidmv1le  47026  hoidmvlelem2  47028  hoidmvlelem3  47029  ovnhoilem1  47033  ovnsubadd2lem  47077  ovolval4lem1  47081  ovolval4lem2  47082  ovolval5lem2  47085  ovnovollem1  47088  ovnovollem2  47089  vonioolem2  47113  vonicclem2  47116  smflim  47209  nsssmfmbflem  47210  smfmullem4  47226  smfsuplem1  47243  smfsuplem3  47245  smflimsuplem3  47254  fsetsnf  47485  cfsetsnfsetf  47492  cfsetsnfsetfo  47494  imasetpreimafvbijlemf  47835  prproropf1o  47941  fmtnodvds  47978  upgrimwlklem2  48332  isubgr3stgrlem6  48405  lincvalsc0  48855  lcoc0  48856  linc0scn0  48857  linc1  48859  lincscm  48864  lincresunit3  48915  1arympt1  49072  1arymaptf  49075  2arympt  49083  2arymaptf  49086  ackendofnn0  49118  amgmlemALT  50236