Theorem fmptd 7067

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3060   ↦ cmpt 5193  ⟶wf 6497

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fun 6503  df-fn 6504  df-f 6505

This theorem is referenced by:  fmpttd  7068  rnmptcOLD  7162  fnwelem  8068  fsetfcdm  8805  fsetfocdm  8806  fdiagfn  8835  resixpfo  8881  xpmapenlem  9095  unxpdomlem3  9203  fsuppmptdm  9325  cantnfp1lem1  9623  cantnfp1lem2  9624  cantnfp1lem3  9625  cantnf  9638  updjudhf  9876  fseqenlem2  9970  dfac8clem  9977  coftr  10218  isf34lem2  10318  axcc2lem  10381  axdc2lem  10393  axdc3lem4  10398  pwcfsdom  10528  rpnnen1lem1  12912  caucvg  15575  sumrblem  15607  summolem2a  15611  supcvg  15752  prodrblem  15823  prodmolem2a  15828  crth  16661  eulerthlem1  16664  prmreclem6  16804  4sqlem11  16838  vdwlem2  16865  vdwlem4  16867  vdwlem6  16869  vdwlem10  16873  ramub1lem2  16910  prmgaplcm  16943  frmdup1  18688  grpinvf  18811  mulgnngsum  18895  cycsubm  19009  cycsubgcl  19013  cycsubgss  19014  conjghm  19053  conjnmz  19056  qusghm  19059  galactghm  19200  symgextf  19213  symgfixf  19232  pmtrdifwrdellem1  19277  odf1  19358  dfod2  19360  pgpssslw  19410  frgpmhm  19561  gsummptfidmsplitres  19722  gsummptfidminv  19738  gsumzunsnd  19747  gsummpt1n0  19756  ablfac1b  19863  ablfac2  19882  abvtrivd  20355  issrngd  20376  pwssplit0  20576  mulgghm2  20934  isphld  21095  pjff  21155  frlmup1  21241  asclf  21322  psr1cl  21408  evlslem1  21529  evlsval2  21534  scmatf  21915  mdetf  21981  maduf  22027  pmatcollpw3fi1lem1  22172  chfacfisf  22240  chfacfisfcpmat  22241  cpmidpmatlem2  22257  lly1stc  22884  txcnmpt  23012  txlm  23036  xkoinjcn  23075  kqffn  23113  txflf  23394  tsmsfbas  23516  ustuqtop0  23629  metdsf  24248  metdsge  24249  mulc1cncf  24305  lebnumlem1  24361  cmetcaulem  24689  ovollb2lem  24889  ovolctb  24891  ovolunlem1a  24897  ovolunlem1  24898  ovoliunlem1  24903  ovoliunlem2  24904  ovoliun  24906  ovolshftlem1  24910  ovolscalem1  24914  ovolicc1  24917  ioombl1lem1  24959  uniioombllem2  24984  volsup2  25006  volcn  25007  vitalilem4  25012  vitalilem5  25013  mbfconst  25034  mbfmax  25050  mbfsup  25065  i1f1lem  25090  i1f1  25091  i1fres  25107  itg1climres  25116  itg2splitlem  25150  itg2split  25151  itg2monolem1  25152  itg2mono  25155  itg2i1fseq  25157  itg2i1fseq2  25158  dvreslem  25310  dvmptresicc  25317  dvivthlem1  25409  dvfsumrlimf  25426  dvfsumlem3  25429  ftc1lem2  25437  ftc1lem6  25442  tdeglem1OLD  25458  radcnvlem1  25809  pserulm  25818  psercn2  25819  abelthlem4  25830  efif1olem4  25938  lgamgulmlem6  26420  gamcvg  26442  basellem4  26470  basellem7  26473  basellem9  26475  lgsfcl2  26688  lgsqrlem2  26732  lgseisenlem1  26760  dchrmusum2  26879  dchrvmasumiflem1  26886  dchrisum0ff  26892  dchrisum0lem1b  26900  dchrisum0lem2a  26902  abvcxp  27000  padicabv  27015  axlowdimlem15  27968  crctcshwlkn0  28829  wlkiswwlks2lem5  28881  wlkswwlksf1o  28887  wwlksnextfun  28906  clwlkclwwlklem2a  29005  clwlkclwwlkf  29015  clwwlkf  29054  frgrncvvdeqlem4  29309  numclwwlk1lem2f  29362  numclwlk2lem2f  29384  ipblnfi  29860  ubthlem1  29875  htthlem  29922  hlimadd  30198  chscllem1  30642  cnlnadjlem2  31073  strlem3a  31257  hstrlem3a  31265  xppreima2  31634  suppovss  31665  fsuppcurry1  31710  fsuppcurry2  31711  pwrssmgc  31930  lmodvslmhm  31962  frobrhm  32138  nsgmgc  32264  elrspunidl  32279  ply1degltdimlem  32404  ply1degltdim  32405  evls1maprhm  32455  rhmpreimacnlem  32554  rhmpreimacn  32555  xrge0mulc1cn  32611  esumpcvgval  32766  esumcvg  32774  mbfmco2  32954  eulerpartlems  33049  erdszelem9  33880  cvmlift3lem3  34002  ex-sategoelel  34102  ex-sategoelelomsuc  34107  elmrsubrn  34201  mvhf  34239  iprodefisum  34400  unbdqndv1  35047  knoppf  35074  ftc1anclem3  36226  ftc1anclem5  36228  lflnegcl  37610  lshpkrcl  37651  tendo0cl  39326  aks6d1c2p1  40621  sticksstones2  40628  sticksstones8  40634  sticksstones9  40635  sticksstones10  40636  sticksstones11  40637  sticksstones12a  40638  sticksstones17  40644  sticksstones18  40645  metakunt1  40650  metakunt2  40651  metakunt19  40668  metakunt25  40674  frlmsnic  40786  rhmmpl  40799  evlsval3  40802  evlsbagval  40806  selvcllem5  40818  cantnfub  41714  binomcxplemradcnv  42754  binomcxplemcvg  42756  binomcxplemnotnn0  42758  projf1o  43539  mullimc  43977  ellimcabssub0  43978  mullimcf  43984  constlimc  43985  idlimc  43987  neglimc  44008  addlimc  44009  0ellimcdiv  44010  fnlimf  44039  liminfpnfuz  44177  xlimpnfxnegmnf2  44219  cncfshift  44235  icccncfext  44248  cncfiooiccre  44256  fprodsubrecnncnvlem  44268  fprodaddrecnncnvlem  44270  ioodvbdlimc1lem1  44292  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  dvnxpaek  44303  dvnprodlem1  44307  itgsinexplem1  44315  itgiccshift  44341  dirkercncflem2  44465  fourierdlem4  44472  fourierdlem5  44473  fourierdlem9  44477  fourierdlem14  44482  fourierdlem16  44484  fourierdlem17  44485  fourierdlem18  44486  fourierdlem21  44489  fourierdlem22  44490  fourierdlem37  44505  fourierdlem50  44517  fourierdlem51  44518  fourierdlem53  44520  fourierdlem55  44522  fourierdlem57  44524  fourierdlem58  44525  fourierdlem59  44526  fourierdlem60  44527  fourierdlem61  44528  fourierdlem67  44534  fourierdlem68  44535  fourierdlem72  44539  fourierdlem73  44540  fourierdlem74  44541  fourierdlem75  44542  fourierdlem76  44543  fourierdlem78  44545  fourierdlem80  44547  fourierdlem81  44548  fourierdlem83  44550  fourierdlem84  44551  fourierdlem88  44555  fourierdlem92  44559  fourierdlem93  44560  fourierdlem97  44564  fourierdlem101  44568  fourierdlem103  44570  fourierdlem104  44571  fourierdlem111  44578  sqwvfoura  44589  elaa2lem  44594  etransclem1  44596  etransclem8  44603  etransclem20  44615  etransclem33  44628  etransclem35  44630  etransclem39  44634  rrxtopnfi  44648  ioorrnopnxrlem  44667  sge0tsms  44741  sge0snmpt  44744  sge0fsummpt  44751  sge0pr  44755  sge0lessmpt  44760  sge0iunmptlemfi  44774  sge0iunmptlemre  44776  sge0iunmpt  44779  sge0rpcpnf  44782  sge0isum  44788  nnfoctbdjlem  44816  psmeasure  44832  voliunsge0lem  44833  meaiuninclem  44841  meaiuninc3v  44845  meaiininclem  44847  omeiunltfirp  44880  carageniuncllem2  44883  caratheodorylem1  44887  caratheodorylem2  44888  isomenndlem  44891  hoicvr  44909  hoicvrrex  44917  ovnsupge0  44918  ovnlecvr  44919  ovnf  44924  ovn0lem  44926  ovnsubaddlem1  44931  ovnsubadd  44933  hsphoif  44937  sge0hsphoire  44950  hoidmv1lelem1  44952  hoidmv1lelem2  44953  hoidmv1lelem3  44954  hoidmv1le  44955  hoidmvlelem2  44957  hoidmvlelem3  44958  ovnhoilem1  44962  ovnsubadd2lem  45006  ovolval4lem1  45010  ovolval4lem2  45011  ovolval5lem2  45014  ovnovollem1  45017  ovnovollem2  45018  vonioolem2  45042  vonicclem2  45045  smflim  45138  nsssmfmbflem  45139  smfmullem4  45155  smfsuplem1  45172  smfsuplem3  45174  smflimsuplem3  45183  fsetsnf  45405  cfsetsnfsetf  45412  cfsetsnfsetfo  45414  imasetpreimafvbijlemf  45713  prproropf1o  45819  fmtnodvds  45856  c0mgm  46327  c0mhm  46328  c0snmgmhm  46332  lincvalsc0  46622  lcoc0  46623  linc0scn0  46624  linc1  46626  lincscm  46631  lincresunit3  46682  1arympt1  46844  1arymaptf  46847  2arympt  46855  2arymaptf  46858  ackendofnn0  46890  amgmlemALT  47370