Theorem fmptd 7109

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3052   ↦ cmpt 5206  ⟶wf 6532

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6538  df-fn 6539  df-f 6540

This theorem is referenced by:  fmpttd  7110  fnwelem  8135  fsetfcdm  8879  fdiagfn  8909  resixpfo  8955  xpmapenlem  9163  unxpdomlem3  9265  fsuppmptdm  9393  cantnfp1lem1  9697  cantnfp1lem2  9698  cantnfp1lem3  9699  cantnf  9712  updjudhf  9950  fseqenlem2  10044  dfac8clem  10051  coftr  10292  isf34lem2  10392  axcc2lem  10455  axdc2lem  10467  axdc3lem4  10472  pwcfsdom  10602  rpnnen1lem1  12999  tpf  14522  caucvg  15700  sumrblem  15732  summolem2a  15736  supcvg  15877  prodrblem  15950  prodmolem2a  15955  crth  16802  eulerthlem1  16805  prmreclem6  16946  4sqlem11  16980  vdwlem2  17007  vdwlem4  17009  vdwlem6  17011  vdwlem10  17015  ramub1lem2  17052  prmgaplcm  17085  frmdup1  18847  grpinvf  18974  mulgnngsum  19067  cycsubm  19190  cycsubgcl  19194  cycsubgss  19195  conjghm  19237  conjnmz  19240  qusghm  19243  galactghm  19390  symgextf  19403  symgfixf  19422  pmtrdifwrdellem1  19467  odf1  19548  dfod2  19550  pgpssslw  19600  frgpmhm  19751  gsummptfidmsplitres  19917  gsummptfidminv  19933  gsumzunsnd  19942  gsummpt1n0  19951  ablfac1b  20058  ablfac2  20077  c0mgm  20424  c0mhm  20425  c0snmgmhm  20427  abvtrivd  20797  issrngd  20820  pwssplit0  21021  rngqiprngimf  21263  mulgghm2  21442  frobrhm  21541  isphld  21619  pjff  21677  frlmup1  21763  asclf  21847  psr1cl  21926  evlslem1  22045  evlsval2  22050  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  24184  metdsf  24793  metdsge  24794  mulc1cncf  24854  lebnumlem1  24916  cmetcaulem  25245  ovollb2lem  25446  ovolctb  25448  ovolunlem1a  25454  ovolunlem1  25455  ovoliunlem1  25460  ovoliunlem2  25461  ovoliun  25463  ovolshftlem1  25467  ovolscalem1  25471  ovolicc1  25474  ioombl1lem1  25516  uniioombllem2  25541  volsup2  25563  volcn  25564  vitalilem4  25569  vitalilem5  25570  mbfconst  25591  mbfmax  25607  mbfsup  25622  i1f1lem  25647  i1f1  25648  i1fres  25663  itg1climres  25672  itg2splitlem  25706  itg2split  25707  itg2monolem1  25708  itg2mono  25711  itg2i1fseq  25713  itg2i1fseq2  25714  dvreslem  25867  dvmptresicc  25874  dvivthlem1  25970  dvfsumrlimf  25988  dvfsumlem3  25992  ftc1lem2  26000  ftc1lem6  26005  radcnvlem1  26379  pserulm  26388  psercn2  26389  psercn2OLD  26390  abelthlem4  26401  efif1olem4  26511  lgamgulmlem6  27001  gamcvg  27023  basellem4  27051  basellem7  27054  basellem9  27056  lgsfcl2  27271  lgsqrlem2  27315  lgseisenlem1  27343  dchrmusum2  27462  dchrvmasumiflem1  27469  dchrisum0ff  27475  dchrisum0lem1b  27483  dchrisum0lem2a  27485  abvcxp  27583  padicabv  27598  axlowdimlem15  28940  crctcshwlkn0  29808  wlkiswwlks2lem5  29860  wlkswwlksf1o  29866  wwlksnextfun  29885  clwlkclwwlklem2a  29984  clwlkclwwlkf  29994  clwwlkf  30033  frgrncvvdeqlem4  30288  numclwwlk1lem2f  30341  numclwlk2lem2f  30363  ipblnfi  30841  ubthlem1  30856  htthlem  30903  hlimadd  31179  chscllem1  31623  cnlnadjlem2  32054  strlem3a  32238  hstrlem3a  32246  xppreima2  32634  suppovss  32663  fsuppcurry1  32707  fsuppcurry2  32708  pwrssmgc  32985  mndlactf1  33026  mndlactfo  33027  mndractf1  33028  mndractfo  33029  lmodvslmhm  33049  rlocf1  33273  nsgmgc  33432  elrspunidl  33448  r1plmhm  33624  r1pquslmic  33625  ply1degltdimlem  33667  ply1degltdim  33668  algextdeglem8  33763  rhmpreimacnlem  33920  rhmpreimacn  33921  xrge0mulc1cn  33977  esumpcvgval  34114  esumcvg  34122  mbfmco2  34302  eulerpartlems  34397  erdszelem9  35226  cvmlift3lem3  35348  ex-sategoelel  35448  ex-sategoelelomsuc  35453  elmrsubrn  35547  mvhf  35585  iprodefisum  35763  unbdqndv1  36531  knoppf  36558  ftc1anclem3  37724  ftc1anclem5  37726  lflnegcl  39098  lshpkrcl  39139  tendo0cl  40814  primrootscoprf  42119  aks6d1c2p1  42136  aks6d1c4  42142  aks6d1c2lem4  42145  aks6d1c2  42148  aks6d1c5lem0  42153  aks6d1c5  42157  sticksstones2  42165  sticksstones8  42171  sticksstones9  42172  sticksstones10  42173  sticksstones11  42174  sticksstones12a  42175  sticksstones17  42181  sticksstones18  42182  aks6d1c6lem2  42189  aks6d1c6lem3  42190  aks6d1c6lem4  42191  aks6d1c6isolem1  42192  aks6d1c6isolem2  42193  aks6d1c6isolem3  42194  aks6d1c6lem5  42195  aks5lem2  42205  frlmsnic  42538  rhmpsr  42550  mplmapghm  42554  evlsval3  42557  evlsbagval  42564  evlsmaprhm  42568  selvcllem5  42580  cantnfub  43320  binomcxplemradcnv  44351  binomcxplemcvg  44353  binomcxplemnotnn0  44355  projf1o  45201  mullimc  45625  ellimcabssub0  45626  mullimcf  45632  constlimc  45633  idlimc  45635  neglimc  45656  addlimc  45657  0ellimcdiv  45658  fnlimf  45687  liminfpnfuz  45825  xlimpnfxnegmnf2  45867  cncfshift  45883  icccncfext  45896  cncfiooiccre  45904  fprodsubrecnncnvlem  45916  fprodaddrecnncnvlem  45918  ioodvbdlimc1lem1  45940  ioodvbdlimc1lem2  45941  ioodvbdlimc2lem  45943  dvnxpaek  45951  dvnprodlem1  45955  itgsinexplem1  45963  itgiccshift  45989  dirkercncflem2  46113  fourierdlem4  46120  fourierdlem5  46121  fourierdlem9  46125  fourierdlem14  46130  fourierdlem16  46132  fourierdlem17  46133  fourierdlem18  46134  fourierdlem21  46137  fourierdlem22  46138  fourierdlem37  46153  fourierdlem50  46165  fourierdlem51  46166  fourierdlem53  46168  fourierdlem55  46170  fourierdlem57  46172  fourierdlem58  46173  fourierdlem59  46174  fourierdlem60  46175  fourierdlem61  46176  fourierdlem67  46182  fourierdlem68  46183  fourierdlem72  46187  fourierdlem73  46188  fourierdlem74  46189  fourierdlem75  46190  fourierdlem76  46191  fourierdlem78  46193  fourierdlem80  46195  fourierdlem81  46196  fourierdlem83  46198  fourierdlem84  46199  fourierdlem88  46203  fourierdlem92  46207  fourierdlem93  46208  fourierdlem97  46212  fourierdlem101  46216  fourierdlem103  46218  fourierdlem104  46219  fourierdlem111  46226  sqwvfoura  46237  elaa2lem  46242  etransclem1  46244  etransclem8  46251  etransclem20  46263  etransclem33  46276  etransclem35  46278  etransclem39  46282  rrxtopnfi  46296  ioorrnopnxrlem  46315  sge0tsms  46389  sge0snmpt  46392  sge0fsummpt  46399  sge0pr  46403  sge0lessmpt  46408  sge0iunmptlemfi  46422  sge0iunmptlemre  46424  sge0iunmpt  46427  sge0rpcpnf  46430  sge0isum  46436  nnfoctbdjlem  46464  psmeasure  46480  voliunsge0lem  46481  meaiuninclem  46489  meaiuninc3v  46493  meaiininclem  46495  omeiunltfirp  46528  carageniuncllem2  46531  caratheodorylem1  46535  caratheodorylem2  46536  isomenndlem  46539  hoicvr  46557  hoicvrrex  46565  ovnsupge0  46566  ovnlecvr  46567  ovnf  46572  ovn0lem  46574  ovnsubaddlem1  46579  ovnsubadd  46581  hsphoif  46585  sge0hsphoire  46598  hoidmv1lelem1  46600  hoidmv1lelem2  46601  hoidmv1lelem3  46602  hoidmv1le  46603  hoidmvlelem2  46605  hoidmvlelem3  46606  ovnhoilem1  46610  ovnsubadd2lem  46654  ovolval4lem1  46658  ovolval4lem2  46659  ovolval5lem2  46662  ovnovollem1  46665  ovnovollem2  46666  vonioolem2  46690  vonicclem2  46693  smflim  46786  nsssmfmbflem  46787  smfmullem4  46803  smfsuplem1  46820  smfsuplem3  46822  smflimsuplem3  46831  fsetsnf  47060  cfsetsnfsetf  47067  cfsetsnfsetfo  47069  imasetpreimafvbijlemf  47395  prproropf1o  47501  fmtnodvds  47538  upgrimwlklem2  47891  isubgr3stgrlem6  47963  lincvalsc0  48377  lcoc0  48378  linc0scn0  48379  linc1  48381  lincscm  48386  lincresunit3  48437  1arympt1  48598  1arymaptf  48601  2arympt  48609  2arymaptf  48612  ackendofnn0  48644  amgmlemALT  49647