Theorem fmptd 7055

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053   ↦ cmpt 5153  ⟶wf 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-fun 6487  df-fn 6488  df-f 6489

This theorem is referenced by:  fmpttd  7056  fnwelem  8071  fsetfcdm  8797  fdiagfn  8828  resixpfo  8874  xpmapenlem  9072  unxpdomlem3  9158  fsuppmptdm  9279  cantnfp1lem1  9590  cantnfp1lem2  9591  cantnfp1lem3  9592  cantnf  9605  updjudhf  9846  fseqenlem2  9938  dfac8clem  9945  coftr  10186  isf34lem2  10286  axcc2lem  10349  axdc2lem  10361  axdc3lem4  10366  pwcfsdom  10497  rpnnen1lem1  12919  tpf  14452  caucvg  15632  sumrblem  15664  summolem2a  15668  supcvg  15812  prodrblem  15885  prodmolem2a  15890  crth  16739  eulerthlem1  16742  prmreclem6  16883  4sqlem11  16917  vdwlem2  16944  vdwlem4  16946  vdwlem6  16948  vdwlem10  16952  ramub1lem2  16989  prmgaplcm  17022  frmdup1  18823  grpinvf  18953  mulgnngsum  19046  cycsubm  19168  cycsubgcl  19172  cycsubgss  19173  conjghm  19215  conjnmz  19218  qusghm  19221  galactghm  19370  symgextf  19383  symgfixf  19402  pmtrdifwrdellem1  19447  odf1  19528  dfod2  19530  pgpssslw  19580  frgpmhm  19731  gsummptfidmsplitres  19897  gsummptfidminv  19913  gsumzunsnd  19922  gsummpt1n0  19931  ablfac1b  20038  ablfac2  20057  c0mgm  20430  c0mhm  20431  c0snmgmhm  20433  abvtrivd  20804  issrngd  20827  pwssplit0  21048  rngqiprngimf  21290  mulgghm2  21451  frobrhm  21550  isphld  21629  pjff  21687  frlmup1  21773  asclf  21856  psr1cl  21935  evlslem1  22058  evlsval2  22063  evlsval3  22065  mplmapghm  22098  evlsmaprhm  22107  selvcllem5  22115  evls1maprhm  22362  rhmmpl  22366  scmatf  22512  mdetf  22578  maduf  22624  pmatcollpw3fi1lem1  22769  chfacfisf  22837  chfacfisfcpmat  22838  cpmidpmatlem2  22854  lly1stc  23479  txcnmpt  23607  txlm  23631  xkoinjcn  23670  kqffn  23708  txflf  23989  tsmsfbas  24111  ustuqtop0  24223  metdsf  24832  metdsge  24833  mulc1cncf  24890  lebnumlem1  24946  cmetcaulem  25273  ovollb2lem  25473  ovolctb  25475  ovolunlem1a  25481  ovolunlem1  25482  ovoliunlem1  25487  ovoliunlem2  25488  ovoliun  25490  ovolshftlem1  25494  ovolscalem1  25498  ovolicc1  25501  ioombl1lem1  25543  uniioombllem2  25568  volsup2  25590  volcn  25591  vitalilem4  25596  vitalilem5  25597  mbfconst  25618  mbfmax  25634  mbfsup  25649  i1f1lem  25674  i1f1  25675  i1fres  25690  itg1climres  25699  itg2splitlem  25733  itg2split  25734  itg2monolem1  25735  itg2mono  25738  itg2i1fseq  25740  itg2i1fseq2  25741  dvreslem  25894  dvmptresicc  25901  dvivthlem1  25993  dvfsumrlimf  26010  dvfsumlem3  26013  ftc1lem2  26021  ftc1lem6  26026  radcnvlem1  26396  pserulm  26405  psercn2  26406  abelthlem4  26417  efif1olem4  26527  lgamgulmlem6  27015  gamcvg  27037  basellem4  27065  basellem7  27068  basellem9  27070  lgsfcl2  27284  lgsqrlem2  27328  lgseisenlem1  27356  dchrmusum2  27475  dchrvmasumiflem1  27482  dchrisum0ff  27488  dchrisum0lem1b  27496  dchrisum0lem2a  27498  abvcxp  27596  padicabv  27611  axlowdimlem15  29043  crctcshwlkn0  29907  wlkiswwlks2lem5  29959  wlkswwlksf1o  29965  wwlksnextfun  29984  clwlkclwwlklem2a  30086  clwlkclwwlkf  30096  clwwlkf  30135  frgrncvvdeqlem4  30390  numclwwlk1lem2f  30443  numclwlk2lem2f  30465  ipblnfi  30944  ubthlem1  30959  htthlem  31006  hlimadd  31282  chscllem1  31726  cnlnadjlem2  32157  strlem3a  32341  hstrlem3a  32349  xppreima2  32743  suppovss  32773  fsuppcurry1  32816  fsuppcurry2  32817  pwrssmgc  33079  mndlactf1  33105  mndlactfo  33106  mndractf1  33107  mndractfo  33108  lmodvslmhm  33131  conjga  33251  rlocf1  33354  nsgmgc  33495  elrspunidl  33511  r1plmhm  33693  r1pquslmic  33694  selvply1rhmlem1  33704  mplvrpmga  33729  mplvrpmmhm  33730  mplvrpmrhm  33731  psrmonprod  33736  mplmonprod  33738  ply1degltdimlem  33806  ply1degltdim  33807  extdgfialglem1  33876  algextdeglem8  33908  rhmpreimacnlem  34068  rhmpreimacn  34069  xrge0mulc1cn  34125  esumpcvgval  34262  esumcvg  34270  mbfmco2  34449  eulerpartlems  34544  erdszelem9  35427  cvmlift3lem3  35549  ex-sategoelel  35649  ex-sategoelelomsuc  35654  elmrsubrn  35748  mvhf  35786  iprodefisum  35969  unbdqndv1  36814  knoppf  36841  ftc1anclem3  38062  ftc1anclem5  38064  lflnegcl  39567  lshpkrcl  39608  tendo0cl  41282  primrootscoprf  42586  aks6d1c2p1  42603  aks6d1c4  42609  aks6d1c2lem4  42612  aks6d1c2  42615  aks6d1c5lem0  42620  aks6d1c5  42624  sticksstones2  42632  sticksstones8  42638  sticksstones9  42639  sticksstones10  42640  sticksstones11  42641  sticksstones12a  42642  sticksstones17  42648  sticksstones18  42649  aks6d1c6lem2  42656  aks6d1c6lem3  42657  aks6d1c6lem4  42658  aks6d1c6isolem1  42659  aks6d1c6isolem2  42660  aks6d1c6isolem3  42661  aks6d1c6lem5  42662  aks5lem2  42672  frlmsnic  43026  rhmpsr  43033  evlsbagval  43036  cantnfub  43766  binomcxplemradcnv  44796  binomcxplemcvg  44798  binomcxplemnotnn0  44800  projf1o  45643  mullimc  46061  ellimcabssub0  46062  mullimcf  46068  constlimc  46069  idlimc  46071  neglimc  46090  addlimc  46091  0ellimcdiv  46092  fnlimf  46121  liminfpnfuz  46259  xlimpnfxnegmnf2  46301  cncfshift  46317  icccncfext  46330  cncfiooiccre  46338  fprodsubrecnncnvlem  46350  fprodaddrecnncnvlem  46352  ioodvbdlimc1lem1  46374  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnxpaek  46385  dvnprodlem1  46389  itgsinexplem1  46397  itgiccshift  46423  dirkercncflem2  46547  fourierdlem4  46554  fourierdlem5  46555  fourierdlem9  46559  fourierdlem14  46564  fourierdlem16  46566  fourierdlem17  46567  fourierdlem18  46568  fourierdlem21  46571  fourierdlem22  46572  fourierdlem37  46587  fourierdlem50  46599  fourierdlem51  46600  fourierdlem53  46602  fourierdlem55  46604  fourierdlem57  46606  fourierdlem58  46607  fourierdlem59  46608  fourierdlem60  46609  fourierdlem61  46610  fourierdlem67  46616  fourierdlem68  46617  fourierdlem72  46621  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem76  46625  fourierdlem78  46627  fourierdlem80  46629  fourierdlem81  46630  fourierdlem83  46632  fourierdlem84  46633  fourierdlem88  46637  fourierdlem92  46641  fourierdlem93  46642  fourierdlem97  46646  fourierdlem101  46650  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  sqwvfoura  46671  elaa2lem  46676  etransclem1  46678  etransclem8  46685  etransclem20  46697  etransclem33  46710  etransclem35  46712  etransclem39  46716  rrxtopnfi  46730  ioorrnopnxrlem  46749  sge0tsms  46823  sge0snmpt  46826  sge0fsummpt  46833  sge0pr  46837  sge0lessmpt  46842  sge0iunmptlemfi  46856  sge0iunmptlemre  46858  sge0iunmpt  46861  sge0rpcpnf  46864  sge0isum  46870  nnfoctbdjlem  46898  psmeasure  46914  voliunsge0lem  46915  meaiuninclem  46923  meaiuninc3v  46927  meaiininclem  46929  omeiunltfirp  46962  carageniuncllem2  46965  caratheodorylem1  46969  caratheodorylem2  46970  isomenndlem  46973  hoicvrrex  46999  ovnsupge0  47000  ovnlecvr  47001  ovnf  47006  ovn0lem  47008  ovnsubaddlem1  47013  ovnsubadd  47015  hsphoif  47019  sge0hsphoire  47032  hoidmv1lelem1  47034  hoidmv1lelem2  47035  hoidmv1lelem3  47036  hoidmv1le  47037  hoidmvlelem2  47039  hoidmvlelem3  47040  ovnhoilem1  47044  ovnsubadd2lem  47088  ovolval4lem1  47092  ovolval4lem2  47093  ovolval5lem2  47096  ovnovollem1  47099  ovnovollem2  47100  vonioolem2  47124  vonicclem2  47127  smflim  47220  nsssmfmbflem  47221  smfmullem4  47237  smfsuplem1  47254  smfsuplem3  47256  smflimsuplem3  47265  fsetsnf  47514  cfsetsnfsetf  47521  cfsetsnfsetfo  47523  imasetpreimafvbijlemf  47876  prproropf1o  47982  fmtnodvds  48022  upgrimwlklem2  48389  isubgr3stgrlem6  48462  lincvalsc0  48912  lcoc0  48913  linc0scn0  48914  linc1  48916  lincscm  48921  lincresunit3  48972  1arympt1  49129  1arymaptf  49132  2arympt  49140  2arymaptf  49143  ackendofnn0  49175  amgmlemALT  50293