Theorem fmptd 7068

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044   ↦ cmpt 5183  ⟶wf 6495

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 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-fun 6501  df-fn 6502  df-f 6503

This theorem is referenced by:  fmpttd  7069  fnwelem  8087  fsetfcdm  8810  fdiagfn  8840  resixpfo  8886  xpmapenlem  9085  unxpdomlem3  9175  fsuppmptdm  9303  cantnfp1lem1  9607  cantnfp1lem2  9608  cantnfp1lem3  9609  cantnf  9622  updjudhf  9860  fseqenlem2  9954  dfac8clem  9961  coftr  10202  isf34lem2  10302  axcc2lem  10365  axdc2lem  10377  axdc3lem4  10382  pwcfsdom  10512  rpnnen1lem1  12913  tpf  14440  caucvg  15621  sumrblem  15653  summolem2a  15657  supcvg  15798  prodrblem  15871  prodmolem2a  15876  crth  16724  eulerthlem1  16727  prmreclem6  16868  4sqlem11  16902  vdwlem2  16929  vdwlem4  16931  vdwlem6  16933  vdwlem10  16937  ramub1lem2  16974  prmgaplcm  17007  frmdup1  18773  grpinvf  18900  mulgnngsum  18993  cycsubm  19116  cycsubgcl  19120  cycsubgss  19121  conjghm  19163  conjnmz  19166  qusghm  19169  galactghm  19318  symgextf  19331  symgfixf  19350  pmtrdifwrdellem1  19395  odf1  19476  dfod2  19478  pgpssslw  19528  frgpmhm  19679  gsummptfidmsplitres  19845  gsummptfidminv  19861  gsumzunsnd  19870  gsummpt1n0  19879  ablfac1b  19986  ablfac2  20005  c0mgm  20379  c0mhm  20380  c0snmgmhm  20382  abvtrivd  20752  issrngd  20775  pwssplit0  20997  rngqiprngimf  21239  mulgghm2  21418  frobrhm  21517  isphld  21596  pjff  21654  frlmup1  21740  asclf  21824  psr1cl  21903  evlslem1  22022  evlsval2  22027  evls1maprhm  22296  rhmmpl  22303  scmatf  22449  mdetf  22515  maduf  22561  pmatcollpw3fi1lem1  22706  chfacfisf  22774  chfacfisfcpmat  22775  cpmidpmatlem2  22791  lly1stc  23416  txcnmpt  23544  txlm  23568  xkoinjcn  23607  kqffn  23645  txflf  23926  tsmsfbas  24048  ustuqtop0  24161  metdsf  24770  metdsge  24771  mulc1cncf  24831  lebnumlem1  24893  cmetcaulem  25221  ovollb2lem  25422  ovolctb  25424  ovolunlem1a  25430  ovolunlem1  25431  ovoliunlem1  25436  ovoliunlem2  25437  ovoliun  25439  ovolshftlem1  25443  ovolscalem1  25447  ovolicc1  25450  ioombl1lem1  25492  uniioombllem2  25517  volsup2  25539  volcn  25540  vitalilem4  25545  vitalilem5  25546  mbfconst  25567  mbfmax  25583  mbfsup  25598  i1f1lem  25623  i1f1  25624  i1fres  25639  itg1climres  25648  itg2splitlem  25682  itg2split  25683  itg2monolem1  25684  itg2mono  25687  itg2i1fseq  25689  itg2i1fseq2  25690  dvreslem  25843  dvmptresicc  25850  dvivthlem1  25946  dvfsumrlimf  25964  dvfsumlem3  25968  ftc1lem2  25976  ftc1lem6  25981  radcnvlem1  26355  pserulm  26364  psercn2  26365  psercn2OLD  26366  abelthlem4  26377  efif1olem4  26487  lgamgulmlem6  26977  gamcvg  26999  basellem4  27027  basellem7  27030  basellem9  27032  lgsfcl2  27247  lgsqrlem2  27291  lgseisenlem1  27319  dchrmusum2  27438  dchrvmasumiflem1  27445  dchrisum0ff  27451  dchrisum0lem1b  27459  dchrisum0lem2a  27461  abvcxp  27559  padicabv  27574  axlowdimlem15  28936  crctcshwlkn0  29801  wlkiswwlks2lem5  29853  wlkswwlksf1o  29859  wwlksnextfun  29878  clwlkclwwlklem2a  29977  clwlkclwwlkf  29987  clwwlkf  30026  frgrncvvdeqlem4  30281  numclwwlk1lem2f  30334  numclwlk2lem2f  30356  ipblnfi  30834  ubthlem1  30849  htthlem  30896  hlimadd  31172  chscllem1  31616  cnlnadjlem2  32047  strlem3a  32231  hstrlem3a  32239  xppreima2  32625  suppovss  32654  fsuppcurry1  32698  fsuppcurry2  32699  pwrssmgc  32972  mndlactf1  33010  mndlactfo  33011  mndractf1  33012  mndractfo  33013  lmodvslmhm  33033  conjga  33142  rlocf1  33240  nsgmgc  33376  elrspunidl  33392  r1plmhm  33568  r1pquslmic  33569  ply1degltdimlem  33611  ply1degltdim  33612  algextdeglem8  33707  rhmpreimacnlem  33867  rhmpreimacn  33868  xrge0mulc1cn  33924  esumpcvgval  34061  esumcvg  34069  mbfmco2  34249  eulerpartlems  34344  erdszelem9  35179  cvmlift3lem3  35301  ex-sategoelel  35401  ex-sategoelelomsuc  35406  elmrsubrn  35500  mvhf  35538  iprodefisum  35721  unbdqndv1  36489  knoppf  36516  ftc1anclem3  37682  ftc1anclem5  37684  lflnegcl  39061  lshpkrcl  39102  tendo0cl  40777  primrootscoprf  42082  aks6d1c2p1  42099  aks6d1c4  42105  aks6d1c2lem4  42108  aks6d1c2  42111  aks6d1c5lem0  42116  aks6d1c5  42120  sticksstones2  42128  sticksstones8  42134  sticksstones9  42135  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones17  42144  sticksstones18  42145  aks6d1c6lem2  42152  aks6d1c6lem3  42153  aks6d1c6lem4  42154  aks6d1c6isolem1  42155  aks6d1c6isolem2  42156  aks6d1c6isolem3  42157  aks6d1c6lem5  42158  aks5lem2  42168  frlmsnic  42521  rhmpsr  42533  mplmapghm  42537  evlsval3  42540  evlsbagval  42547  evlsmaprhm  42551  selvcllem5  42563  cantnfub  43303  binomcxplemradcnv  44334  binomcxplemcvg  44336  binomcxplemnotnn0  44338  projf1o  45184  mullimc  45607  ellimcabssub0  45608  mullimcf  45614  constlimc  45615  idlimc  45617  neglimc  45638  addlimc  45639  0ellimcdiv  45640  fnlimf  45669  liminfpnfuz  45807  xlimpnfxnegmnf2  45849  cncfshift  45865  icccncfext  45878  cncfiooiccre  45886  fprodsubrecnncnvlem  45898  fprodaddrecnncnvlem  45900  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnxpaek  45933  dvnprodlem1  45937  itgsinexplem1  45945  itgiccshift  45971  dirkercncflem2  46095  fourierdlem4  46102  fourierdlem5  46103  fourierdlem9  46107  fourierdlem14  46112  fourierdlem16  46114  fourierdlem17  46115  fourierdlem18  46116  fourierdlem21  46119  fourierdlem22  46120  fourierdlem37  46135  fourierdlem50  46147  fourierdlem51  46148  fourierdlem53  46150  fourierdlem55  46152  fourierdlem57  46154  fourierdlem58  46155  fourierdlem59  46156  fourierdlem60  46157  fourierdlem61  46158  fourierdlem67  46164  fourierdlem68  46165  fourierdlem72  46169  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem78  46175  fourierdlem80  46177  fourierdlem81  46178  fourierdlem83  46180  fourierdlem84  46181  fourierdlem88  46185  fourierdlem92  46189  fourierdlem93  46190  fourierdlem97  46194  fourierdlem101  46198  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  sqwvfoura  46219  elaa2lem  46224  etransclem1  46226  etransclem8  46233  etransclem20  46245  etransclem33  46258  etransclem35  46260  etransclem39  46264  rrxtopnfi  46278  ioorrnopnxrlem  46297  sge0tsms  46371  sge0snmpt  46374  sge0fsummpt  46381  sge0pr  46385  sge0lessmpt  46390  sge0iunmptlemfi  46404  sge0iunmptlemre  46406  sge0iunmpt  46409  sge0rpcpnf  46412  sge0isum  46418  nnfoctbdjlem  46446  psmeasure  46462  voliunsge0lem  46463  meaiuninclem  46471  meaiuninc3v  46475  meaiininclem  46477  omeiunltfirp  46510  carageniuncllem2  46513  caratheodorylem1  46517  caratheodorylem2  46518  isomenndlem  46521  hoicvr  46539  hoicvrrex  46547  ovnsupge0  46548  ovnlecvr  46549  ovnf  46554  ovn0lem  46556  ovnsubaddlem1  46561  ovnsubadd  46563  hsphoif  46567  sge0hsphoire  46580  hoidmv1lelem1  46582  hoidmv1lelem2  46583  hoidmv1lelem3  46584  hoidmv1le  46585  hoidmvlelem2  46587  hoidmvlelem3  46588  ovnhoilem1  46592  ovnsubadd2lem  46636  ovolval4lem1  46640  ovolval4lem2  46641  ovolval5lem2  46644  ovnovollem1  46647  ovnovollem2  46648  vonioolem2  46672  vonicclem2  46675  smflim  46768  nsssmfmbflem  46769  smfmullem4  46785  smfsuplem1  46802  smfsuplem3  46804  smflimsuplem3  46813  fsetsnf  47045  cfsetsnfsetf  47052  cfsetsnfsetfo  47054  imasetpreimafvbijlemf  47395  prproropf1o  47501  fmtnodvds  47538  upgrimwlklem2  47891  isubgr3stgrlem6  47963  lincvalsc0  48403  lcoc0  48404  linc0scn0  48405  linc1  48407  lincscm  48412  lincresunit3  48463  1arympt1  48620  1arymaptf  48623  2arympt  48631  2arymaptf  48634  ackendofnn0  48666  amgmlemALT  49785