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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079   ↦ cmpt 5192  ⟶wf 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-fun 6538  df-fn 6539  df-f 6540

This theorem is referenced by:  fmpttd  7110  fnwelem  8123  fsetfcdm  8853  fdiagfn  8884  resixpfo  8930  xpmapenlem  9128  unxpdomlem3  9214  fsuppmptdm  9332  cantnfp1lem1  9643  cantnfp1lem2  9644  cantnfp1lem3  9645  cantnf  9658  updjudhf  9913  fseqenlem2  10005  dfac8clem  10012  coftr  10252  isf34lem2  10352  axcc2lem  10415  axdc2lem  10427  axdc3lem4  10432  pwcfsdom  10563  rpnnen1lem1  12997  tpf  14532  caucvg  15726  sumrblem  15758  summolem2a  15762  supcvg  15906  prodrblem  15979  prodmolem2a  15984  crth  16832  eulerthlem1  16835  prmreclem6  16976  4sqlem11  17010  vdwlem2  17037  vdwlem4  17039  vdwlem6  17041  vdwlem10  17045  ramub1lem2  17082  prmgaplcm  17115  frmdup1  18918  grpinvf  19048  mulgnngsum  19140  cycsubm  19268  cycsubgcl  19272  cycsubgss  19273  conjghm  19314  conjnmz  19317  qusghm  19320  galactghm  19469  symgextf  19482  symgfixf  19501  pmtrdifwrdellem1  19546  odf1  19627  dfod2  19629  pgpssslw  19679  frgpmhm  19830  gsummptfidmsplitres  19996  gsummptfidminv  20012  gsumzunsnd  20021  gsummpt1n0  20030  ablfac1b  20137  ablfac2  20156  c0mgm  20537  c0mhm  20538  c0snmgmhm  20540  abvtrivd  20935  issrngd  20958  pwssplit0  21179  rngqiprngimf  21437  mulgghm2  21626  frobrhm  21725  isphld  21804  pjff  21862  frlmup1  21948  asclf  22031  psr1cl  22110  evlslem1  22233  evlsval2  22238  evlsval3  22240  mplmapghm  22273  evlsmaprhm  22282  selvcllem5  22290  evls1maprhm  22536  rhmmpl  22540  scmatf  22686  mdetf  22752  maduf  22798  pmatcollpw3fi1lem1  22943  chfacfisf  23011  chfacfisfcpmat  23012  cpmidpmatlem2  23028  lly1stc  23653  txcnmpt  23781  txlm  23805  xkoinjcn  23844  kqffn  23882  txflf  24163  tsmsfbas  24285  ustuqtop0  24397  metdsf  25006  metdsge  25007  mulc1cncf  25064  lebnumlem1  25120  cmetcaulem  25447  ovollb2lem  25647  ovolctb  25649  ovolunlem1a  25655  ovolunlem1  25656  ovoliunlem1  25661  ovoliunlem2  25662  ovoliun  25664  ovolshftlem1  25668  ovolscalem1  25672  ovolicc1  25675  ioombl1lem1  25717  uniioombllem2  25742  volsup2  25764  volcn  25765  vitalilem4  25770  vitalilem5  25771  mbfconst  25792  mbfmax  25808  mbfsup  25823  i1f1lem  25848  i1f1  25849  i1fres  25864  itg1climres  25873  itg2splitlem  25907  itg2split  25908  itg2monolem1  25909  itg2mono  25912  itg2i1fseq  25914  itg2i1fseq2  25915  dvreslem  26068  dvmptresicc  26075  dvivthlem1  26167  dvfsumrlimf  26184  dvfsumlem3  26187  ftc1lem2  26195  ftc1lem6  26200  radcnvlem1  26576  pserulm  26585  psercn2  26586  abelthlem4  26597  efif1olem4  26710  lgamgulmlem6  27198  gamcvg  27220  basellem4  27248  basellem7  27251  basellem9  27253  lgsfcl2  27467  lgsqrlem2  27511  lgseisenlem1  27539  dchrmusum2  27658  dchrvmasumiflem1  27665  dchrisum0ff  27671  dchrisum0lem1b  27679  dchrisum0lem2a  27681  abvcxp  27779  padicabv  27794  axlowdimlem15  29306  crctcshwlkn0  30170  wlkiswwlks2lem5  30222  wlkswwlksf1o  30228  wwlksnextfun  30247  clwlkclwwlklem2a  30349  clwlkclwwlkf  30359  clwwlkf  30398  frgrncvvdeqlem4  30653  numclwwlk1lem2f  30706  numclwlk2lem2f  30728  ipblnfi  31207  ubthlem1  31222  htthlem  31269  hlimadd  31545  chscllem1  31989  cnlnadjlem2  32420  strlem3a  32604  hstrlem3a  32612  xppreima2  32996  suppovss  33026  fsuppcurry1  33069  fsuppcurry2  33070  pwrssmgc  33320  mndlactf1  33346  mndlactfo  33347  mndractf1  33348  mndractfo  33349  lmodvslmhm  33370  conjga  33490  rlocf1  33594  nsgmgc  33721  elrspunidl  33736  r1plmhm  33899  r1pquslmic  33900  selvply1rhmlem1  33910  mplvrpmga  33935  mplvrpmmhm  33936  mplvrpmrhm  33937  psrmonprod  33942  mplmonprod  33944  ply1degltdimlem  34012  ply1degltdim  34013  extdgfialglem1  34082  algextdeglem8  34114  rhmpreimacnlem  34274  rhmpreimacn  34275  xrge0mulc1cn  34331  esumpcvgval  34468  esumcvg  34476  mbfmco2  34655  eulerpartlems  34750  onvfowev  35600  erdszelem9  35691  cvmlift3lem3  35813  ex-sategoelel  35913  ex-sategoelelomsuc  35918  elmrsubrn  36012  mvhf  36050  iprodefisum  36233  unbdqndv1  37097  knoppf  37124  ftc1anclem3  38346  ftc1anclem5  38348  lflnegcl  39849  lshpkrcl  39890  tendo0cl  41564  primrootscoprf  42868  aks6d1c2p1  42885  aks6d1c4  42891  aks6d1c2lem4  42894  aks6d1c2  42897  aks6d1c5lem0  42902  aks6d1c5  42906  sticksstones2  42914  sticksstones8  42920  sticksstones9  42921  sticksstones10  42922  sticksstones11  42923  sticksstones12a  42924  sticksstones17  42930  sticksstones18  42931  aks6d1c6lem2  42938  aks6d1c6lem3  42939  aks6d1c6lem4  42940  aks6d1c6isolem1  42941  aks6d1c6isolem2  42942  aks6d1c6isolem3  42943  aks6d1c6lem5  42944  aks5lem2  42954  frlmsnic  43308  rhmpsr  43315  evlsbagval  43318  cantnfub  44048  binomcxplemradcnv  45062  binomcxplemcvg  45064  binomcxplemnotnn0  45066  projf1o  45914  mullimc  46332  ellimcabssub0  46333  mullimcf  46339  constlimc  46340  idlimc  46342  neglimc  46361  addlimc  46362  0ellimcdiv  46363  fnlimf  46392  liminfpnfuz  46530  xlimpnfxnegmnf2  46572  cncfshift  46588  icccncfext  46601  cncfiooiccre  46609  fprodsubrecnncnvlem  46621  fprodaddrecnncnvlem  46623  ioodvbdlimc1lem1  46645  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  dvnxpaek  46656  dvnprodlem1  46660  itgsinexplem1  46668  itgiccshift  46694  dirkercncflem2  46818  fourierdlem4  46825  fourierdlem5  46826  fourierdlem9  46830  fourierdlem14  46835  fourierdlem16  46837  fourierdlem17  46838  fourierdlem18  46839  fourierdlem21  46842  fourierdlem22  46843  fourierdlem37  46858  fourierdlem50  46870  fourierdlem51  46871  fourierdlem53  46873  fourierdlem55  46875  fourierdlem57  46877  fourierdlem58  46878  fourierdlem59  46879  fourierdlem60  46880  fourierdlem61  46881  fourierdlem67  46887  fourierdlem68  46888  fourierdlem72  46892  fourierdlem73  46893  fourierdlem74  46894  fourierdlem75  46895  fourierdlem76  46896  fourierdlem78  46898  fourierdlem80  46900  fourierdlem81  46901  fourierdlem83  46903  fourierdlem84  46904  fourierdlem88  46908  fourierdlem92  46912  fourierdlem93  46913  fourierdlem97  46917  fourierdlem101  46921  fourierdlem103  46923  fourierdlem104  46924  fourierdlem111  46931  sqwvfoura  46942  elaa2lem  46947  etransclem1  46949  etransclem8  46956  etransclem20  46968  etransclem33  46981  etransclem35  46983  etransclem39  46987  rrxtopnfi  47001  ioorrnopnxrlem  47020  sge0tsms  47094  sge0snmpt  47097  sge0fsummpt  47104  sge0pr  47108  sge0lessmpt  47113  sge0iunmptlemfi  47127  sge0iunmptlemre  47129  sge0iunmpt  47132  sge0rpcpnf  47135  sge0isum  47141  nnfoctbdjlem  47169  psmeasure  47185  voliunsge0lem  47186  meaiuninclem  47194  meaiuninc3v  47198  meaiininclem  47200  omeiunltfirp  47233  carageniuncllem2  47236  caratheodorylem1  47240  caratheodorylem2  47241  isomenndlem  47244  hoicvrrex  47270  ovnsupge0  47271  ovnlecvr  47272  ovnf  47277  ovn0lem  47279  ovnsubaddlem1  47284  ovnsubadd  47286  hsphoif  47290  sge0hsphoire  47303  hoidmv1lelem1  47305  hoidmv1lelem2  47306  hoidmv1lelem3  47307  hoidmv1le  47308  hoidmvlelem2  47310  hoidmvlelem3  47311  ovnhoilem1  47315  ovnsubadd2lem  47359  ovolval4lem1  47363  ovolval4lem2  47364  ovolval5lem2  47367  ovnovollem1  47370  ovnovollem2  47371  vonioolem2  47395  vonicclem2  47398  smflim  47491  nsssmfmbflem  47492  smfmullem4  47508  smfsuplem1  47525  smfsuplem3  47527  smflimsuplem3  47536  fsetsnf  47788  cfsetsnfsetf  47795  cfsetsnfsetfo  47797  imasetpreimafvbijlemf  48150  prproropf1o  48256  fmtnodvds  48296  upgrimwlklem2  48663  isubgr3stgrlem6  48736  lincvalsc0  49201  lcoc0  49202  linc0scn0  49203  linc1  49205  lincscm  49210  lincresunit3  49261  1arympt1  49418  1arymaptf  49421  2arympt  49429  2arymaptf  49432  ackendofnn0  49464  amgmlemALT  50623