Theorem fmptd 7057

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3049   ↦ cmpt 5177  ⟶wf 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-fun 6492  df-fn 6493  df-f 6494

This theorem is referenced by:  fmpttd  7058  fnwelem  8071  fsetfcdm  8795  fdiagfn  8826  resixpfo  8872  xpmapenlem  9070  unxpdomlem3  9156  fsuppmptdm  9277  cantnfp1lem1  9585  cantnfp1lem2  9586  cantnfp1lem3  9587  cantnf  9600  updjudhf  9841  fseqenlem2  9933  dfac8clem  9940  coftr  10181  isf34lem2  10281  axcc2lem  10344  axdc2lem  10356  axdc3lem4  10361  pwcfsdom  10492  rpnnen1lem1  12889  tpf  14420  caucvg  15600  sumrblem  15632  summolem2a  15636  supcvg  15777  prodrblem  15850  prodmolem2a  15855  crth  16703  eulerthlem1  16706  prmreclem6  16847  4sqlem11  16881  vdwlem2  16908  vdwlem4  16910  vdwlem6  16912  vdwlem10  16916  ramub1lem2  16953  prmgaplcm  16986  frmdup1  18787  grpinvf  18914  mulgnngsum  19007  cycsubm  19129  cycsubgcl  19133  cycsubgss  19134  conjghm  19176  conjnmz  19179  qusghm  19182  galactghm  19331  symgextf  19344  symgfixf  19363  pmtrdifwrdellem1  19408  odf1  19489  dfod2  19491  pgpssslw  19541  frgpmhm  19692  gsummptfidmsplitres  19858  gsummptfidminv  19874  gsumzunsnd  19883  gsummpt1n0  19892  ablfac1b  19999  ablfac2  20018  c0mgm  20393  c0mhm  20394  c0snmgmhm  20396  abvtrivd  20763  issrngd  20786  pwssplit0  21008  rngqiprngimf  21250  mulgghm2  21429  frobrhm  21528  isphld  21607  pjff  21665  frlmup1  21751  asclf  21835  psr1cl  21914  evlslem1  22035  evlsval2  22040  evlsval3  22042  evls1maprhm  22318  rhmmpl  22325  scmatf  22471  mdetf  22537  maduf  22583  pmatcollpw3fi1lem1  22728  chfacfisf  22796  chfacfisfcpmat  22797  cpmidpmatlem2  22813  lly1stc  23438  txcnmpt  23566  txlm  23590  xkoinjcn  23629  kqffn  23667  txflf  23948  tsmsfbas  24070  ustuqtop0  24182  metdsf  24791  metdsge  24792  mulc1cncf  24852  lebnumlem1  24914  cmetcaulem  25242  ovollb2lem  25443  ovolctb  25445  ovolunlem1a  25451  ovolunlem1  25452  ovoliunlem1  25457  ovoliunlem2  25458  ovoliun  25460  ovolshftlem1  25464  ovolscalem1  25468  ovolicc1  25471  ioombl1lem1  25513  uniioombllem2  25538  volsup2  25560  volcn  25561  vitalilem4  25566  vitalilem5  25567  mbfconst  25588  mbfmax  25604  mbfsup  25619  i1f1lem  25644  i1f1  25645  i1fres  25660  itg1climres  25669  itg2splitlem  25703  itg2split  25704  itg2monolem1  25705  itg2mono  25708  itg2i1fseq  25710  itg2i1fseq2  25711  dvreslem  25864  dvmptresicc  25871  dvivthlem1  25967  dvfsumrlimf  25985  dvfsumlem3  25989  ftc1lem2  25997  ftc1lem6  26002  radcnvlem1  26376  pserulm  26385  psercn2  26386  psercn2OLD  26387  abelthlem4  26398  efif1olem4  26508  lgamgulmlem6  26998  gamcvg  27020  basellem4  27048  basellem7  27051  basellem9  27053  lgsfcl2  27268  lgsqrlem2  27312  lgseisenlem1  27340  dchrmusum2  27459  dchrvmasumiflem1  27466  dchrisum0ff  27472  dchrisum0lem1b  27480  dchrisum0lem2a  27482  abvcxp  27580  padicabv  27595  axlowdimlem15  28978  crctcshwlkn0  29843  wlkiswwlks2lem5  29895  wlkswwlksf1o  29901  wwlksnextfun  29920  clwlkclwwlklem2a  30022  clwlkclwwlkf  30032  clwwlkf  30071  frgrncvvdeqlem4  30326  numclwwlk1lem2f  30379  numclwlk2lem2f  30401  ipblnfi  30879  ubthlem1  30894  htthlem  30941  hlimadd  31217  chscllem1  31661  cnlnadjlem2  32092  strlem3a  32276  hstrlem3a  32284  xppreima2  32678  suppovss  32709  fsuppcurry1  32752  fsuppcurry2  32753  pwrssmgc  33031  mndlactf1  33057  mndlactfo  33058  mndractf1  33059  mndractfo  33060  lmodvslmhm  33082  conjga  33201  rlocf1  33304  nsgmgc  33442  elrspunidl  33458  r1plmhm  33640  r1pquslmic  33641  mplvrpmga  33659  mplvrpmmhm  33660  mplvrpmrhm  33661  ply1degltdimlem  33728  ply1degltdim  33729  extdgfialglem1  33798  algextdeglem8  33830  rhmpreimacnlem  33990  rhmpreimacn  33991  xrge0mulc1cn  34047  esumpcvgval  34184  esumcvg  34192  mbfmco2  34371  eulerpartlems  34466  erdszelem9  35342  cvmlift3lem3  35464  ex-sategoelel  35564  ex-sategoelelomsuc  35569  elmrsubrn  35663  mvhf  35701  iprodefisum  35884  unbdqndv1  36651  knoppf  36678  ftc1anclem3  37835  ftc1anclem5  37837  lflnegcl  39274  lshpkrcl  39315  tendo0cl  40989  primrootscoprf  42294  aks6d1c2p1  42311  aks6d1c4  42317  aks6d1c2lem4  42320  aks6d1c2  42323  aks6d1c5lem0  42328  aks6d1c5  42332  sticksstones2  42340  sticksstones8  42346  sticksstones9  42347  sticksstones10  42348  sticksstones11  42349  sticksstones12a  42350  sticksstones17  42356  sticksstones18  42357  aks6d1c6lem2  42364  aks6d1c6lem3  42365  aks6d1c6lem4  42366  aks6d1c6isolem1  42367  aks6d1c6isolem2  42368  aks6d1c6isolem3  42369  aks6d1c6lem5  42370  aks5lem2  42380  frlmsnic  42737  rhmpsr  42747  mplmapghm  42749  evlsbagval  42754  evlsmaprhm  42758  selvcllem5  42767  cantnfub  43505  binomcxplemradcnv  44535  binomcxplemcvg  44537  binomcxplemnotnn0  44539  projf1o  45383  mullimc  45804  ellimcabssub0  45805  mullimcf  45811  constlimc  45812  idlimc  45814  neglimc  45833  addlimc  45834  0ellimcdiv  45835  fnlimf  45864  liminfpnfuz  46002  xlimpnfxnegmnf2  46044  cncfshift  46060  icccncfext  46073  cncfiooiccre  46081  fprodsubrecnncnvlem  46093  fprodaddrecnncnvlem  46095  ioodvbdlimc1lem1  46117  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  dvnxpaek  46128  dvnprodlem1  46132  itgsinexplem1  46140  itgiccshift  46166  dirkercncflem2  46290  fourierdlem4  46297  fourierdlem5  46298  fourierdlem9  46302  fourierdlem14  46307  fourierdlem16  46309  fourierdlem17  46310  fourierdlem18  46311  fourierdlem21  46314  fourierdlem22  46315  fourierdlem37  46330  fourierdlem50  46342  fourierdlem51  46343  fourierdlem53  46345  fourierdlem55  46347  fourierdlem57  46349  fourierdlem58  46350  fourierdlem59  46351  fourierdlem60  46352  fourierdlem61  46353  fourierdlem67  46359  fourierdlem68  46360  fourierdlem72  46364  fourierdlem73  46365  fourierdlem74  46366  fourierdlem75  46367  fourierdlem76  46368  fourierdlem78  46370  fourierdlem80  46372  fourierdlem81  46373  fourierdlem83  46375  fourierdlem84  46376  fourierdlem88  46380  fourierdlem92  46384  fourierdlem93  46385  fourierdlem97  46389  fourierdlem101  46393  fourierdlem103  46395  fourierdlem104  46396  fourierdlem111  46403  sqwvfoura  46414  elaa2lem  46419  etransclem1  46421  etransclem8  46428  etransclem20  46440  etransclem33  46453  etransclem35  46455  etransclem39  46459  rrxtopnfi  46473  ioorrnopnxrlem  46492  sge0tsms  46566  sge0snmpt  46569  sge0fsummpt  46576  sge0pr  46580  sge0lessmpt  46585  sge0iunmptlemfi  46599  sge0iunmptlemre  46601  sge0iunmpt  46604  sge0rpcpnf  46607  sge0isum  46613  nnfoctbdjlem  46641  psmeasure  46657  voliunsge0lem  46658  meaiuninclem  46666  meaiuninc3v  46670  meaiininclem  46672  omeiunltfirp  46705  carageniuncllem2  46708  caratheodorylem1  46712  caratheodorylem2  46713  isomenndlem  46716  hoicvr  46734  hoicvrrex  46742  ovnsupge0  46743  ovnlecvr  46744  ovnf  46749  ovn0lem  46751  ovnsubaddlem1  46756  ovnsubadd  46758  hsphoif  46762  sge0hsphoire  46775  hoidmv1lelem1  46777  hoidmv1lelem2  46778  hoidmv1lelem3  46779  hoidmv1le  46780  hoidmvlelem2  46782  hoidmvlelem3  46783  ovnhoilem1  46787  ovnsubadd2lem  46831  ovolval4lem1  46835  ovolval4lem2  46836  ovolval5lem2  46839  ovnovollem1  46842  ovnovollem2  46843  vonioolem2  46867  vonicclem2  46870  smflim  46963  nsssmfmbflem  46964  smfmullem4  46980  smfsuplem1  46997  smfsuplem3  46999  smflimsuplem3  47008  fsetsnf  47239  cfsetsnfsetf  47246  cfsetsnfsetfo  47248  imasetpreimafvbijlemf  47589  prproropf1o  47695  fmtnodvds  47732  upgrimwlklem2  48086  isubgr3stgrlem6  48159  lincvalsc0  48609  lcoc0  48610  linc0scn0  48611  linc1  48613  lincscm  48618  lincresunit3  48669  1arympt1  48826  1arymaptf  48829  2arympt  48837  2arymaptf  48840  ackendofnn0  48872  amgmlemALT  49990