Theorem fmptd 7103

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3051   ↦ cmpt 5201  ⟶wf 6526

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-fun 6532  df-fn 6533  df-f 6534

This theorem is referenced by:  fmpttd  7104  fnwelem  8128  fsetfcdm  8872  fdiagfn  8902  resixpfo  8948  xpmapenlem  9156  unxpdomlem3  9258  fsuppmptdm  9386  cantnfp1lem1  9690  cantnfp1lem2  9691  cantnfp1lem3  9692  cantnf  9705  updjudhf  9943  fseqenlem2  10037  dfac8clem  10044  coftr  10285  isf34lem2  10385  axcc2lem  10448  axdc2lem  10460  axdc3lem4  10465  pwcfsdom  10595  rpnnen1lem1  12992  tpf  14515  caucvg  15693  sumrblem  15725  summolem2a  15729  supcvg  15870  prodrblem  15943  prodmolem2a  15948  crth  16795  eulerthlem1  16798  prmreclem6  16939  4sqlem11  16973  vdwlem2  17000  vdwlem4  17002  vdwlem6  17004  vdwlem10  17008  ramub1lem2  17045  prmgaplcm  17078  frmdup1  18840  grpinvf  18967  mulgnngsum  19060  cycsubm  19183  cycsubgcl  19187  cycsubgss  19188  conjghm  19230  conjnmz  19233  qusghm  19236  galactghm  19383  symgextf  19396  symgfixf  19415  pmtrdifwrdellem1  19460  odf1  19541  dfod2  19543  pgpssslw  19593  frgpmhm  19744  gsummptfidmsplitres  19910  gsummptfidminv  19926  gsumzunsnd  19935  gsummpt1n0  19944  ablfac1b  20051  ablfac2  20070  c0mgm  20417  c0mhm  20418  c0snmgmhm  20420  abvtrivd  20790  issrngd  20813  pwssplit0  21014  rngqiprngimf  21256  mulgghm2  21435  frobrhm  21534  isphld  21612  pjff  21670  frlmup1  21756  asclf  21840  psr1cl  21919  evlslem1  22038  evlsval2  22043  evls1maprhm  22312  rhmmpl  22319  scmatf  22465  mdetf  22531  maduf  22577  pmatcollpw3fi1lem1  22722  chfacfisf  22790  chfacfisfcpmat  22791  cpmidpmatlem2  22807  lly1stc  23432  txcnmpt  23560  txlm  23584  xkoinjcn  23623  kqffn  23661  txflf  23942  tsmsfbas  24064  ustuqtop0  24177  metdsf  24786  metdsge  24787  mulc1cncf  24847  lebnumlem1  24909  cmetcaulem  25238  ovollb2lem  25439  ovolctb  25441  ovolunlem1a  25447  ovolunlem1  25448  ovoliunlem1  25453  ovoliunlem2  25454  ovoliun  25456  ovolshftlem1  25460  ovolscalem1  25464  ovolicc1  25467  ioombl1lem1  25509  uniioombllem2  25534  volsup2  25556  volcn  25557  vitalilem4  25562  vitalilem5  25563  mbfconst  25584  mbfmax  25600  mbfsup  25615  i1f1lem  25640  i1f1  25641  i1fres  25656  itg1climres  25665  itg2splitlem  25699  itg2split  25700  itg2monolem1  25701  itg2mono  25704  itg2i1fseq  25706  itg2i1fseq2  25707  dvreslem  25860  dvmptresicc  25867  dvivthlem1  25963  dvfsumrlimf  25981  dvfsumlem3  25985  ftc1lem2  25993  ftc1lem6  25998  radcnvlem1  26372  pserulm  26381  psercn2  26382  psercn2OLD  26383  abelthlem4  26394  efif1olem4  26504  lgamgulmlem6  26994  gamcvg  27016  basellem4  27044  basellem7  27047  basellem9  27049  lgsfcl2  27264  lgsqrlem2  27308  lgseisenlem1  27336  dchrmusum2  27455  dchrvmasumiflem1  27462  dchrisum0ff  27468  dchrisum0lem1b  27476  dchrisum0lem2a  27478  abvcxp  27576  padicabv  27591  axlowdimlem15  28881  crctcshwlkn0  29749  wlkiswwlks2lem5  29801  wlkswwlksf1o  29807  wwlksnextfun  29826  clwlkclwwlklem2a  29925  clwlkclwwlkf  29935  clwwlkf  29974  frgrncvvdeqlem4  30229  numclwwlk1lem2f  30282  numclwlk2lem2f  30304  ipblnfi  30782  ubthlem1  30797  htthlem  30844  hlimadd  31120  chscllem1  31564  cnlnadjlem2  31995  strlem3a  32179  hstrlem3a  32187  xppreima2  32575  suppovss  32604  fsuppcurry1  32648  fsuppcurry2  32649  pwrssmgc  32926  mndlactf1  32967  mndlactfo  32968  mndractf1  32969  mndractfo  32970  lmodvslmhm  32990  rlocf1  33214  nsgmgc  33373  elrspunidl  33389  r1plmhm  33565  r1pquslmic  33566  ply1degltdimlem  33608  ply1degltdim  33609  algextdeglem8  33704  rhmpreimacnlem  33861  rhmpreimacn  33862  xrge0mulc1cn  33918  esumpcvgval  34055  esumcvg  34063  mbfmco2  34243  eulerpartlems  34338  erdszelem9  35167  cvmlift3lem3  35289  ex-sategoelel  35389  ex-sategoelelomsuc  35394  elmrsubrn  35488  mvhf  35526  iprodefisum  35704  unbdqndv1  36472  knoppf  36499  ftc1anclem3  37665  ftc1anclem5  37667  lflnegcl  39039  lshpkrcl  39080  tendo0cl  40755  primrootscoprf  42060  aks6d1c2p1  42077  aks6d1c4  42083  aks6d1c2lem4  42086  aks6d1c2  42089  aks6d1c5lem0  42094  aks6d1c5  42098  sticksstones2  42106  sticksstones8  42112  sticksstones9  42113  sticksstones10  42114  sticksstones11  42115  sticksstones12a  42116  sticksstones17  42122  sticksstones18  42123  aks6d1c6lem2  42130  aks6d1c6lem3  42131  aks6d1c6lem4  42132  aks6d1c6isolem1  42133  aks6d1c6isolem2  42134  aks6d1c6isolem3  42135  aks6d1c6lem5  42136  aks5lem2  42146  metakunt1  42164  metakunt2  42165  metakunt19  42182  metakunt25  42188  frlmsnic  42510  rhmpsr  42522  mplmapghm  42526  evlsval3  42529  evlsbagval  42536  evlsmaprhm  42540  selvcllem5  42552  cantnfub  43292  binomcxplemradcnv  44324  binomcxplemcvg  44326  binomcxplemnotnn0  44328  projf1o  45169  mullimc  45593  ellimcabssub0  45594  mullimcf  45600  constlimc  45601  idlimc  45603  neglimc  45624  addlimc  45625  0ellimcdiv  45626  fnlimf  45655  liminfpnfuz  45793  xlimpnfxnegmnf2  45835  cncfshift  45851  icccncfext  45864  cncfiooiccre  45872  fprodsubrecnncnvlem  45884  fprodaddrecnncnvlem  45886  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnxpaek  45919  dvnprodlem1  45923  itgsinexplem1  45931  itgiccshift  45957  dirkercncflem2  46081  fourierdlem4  46088  fourierdlem5  46089  fourierdlem9  46093  fourierdlem14  46098  fourierdlem16  46100  fourierdlem17  46101  fourierdlem18  46102  fourierdlem21  46105  fourierdlem22  46106  fourierdlem37  46121  fourierdlem50  46133  fourierdlem51  46134  fourierdlem53  46136  fourierdlem55  46138  fourierdlem57  46140  fourierdlem58  46141  fourierdlem59  46142  fourierdlem60  46143  fourierdlem61  46144  fourierdlem67  46150  fourierdlem68  46151  fourierdlem72  46155  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem78  46161  fourierdlem80  46163  fourierdlem81  46164  fourierdlem83  46166  fourierdlem84  46167  fourierdlem88  46171  fourierdlem92  46175  fourierdlem93  46176  fourierdlem97  46180  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  sqwvfoura  46205  elaa2lem  46210  etransclem1  46212  etransclem8  46219  etransclem20  46231  etransclem33  46244  etransclem35  46246  etransclem39  46250  rrxtopnfi  46264  ioorrnopnxrlem  46283  sge0tsms  46357  sge0snmpt  46360  sge0fsummpt  46367  sge0pr  46371  sge0lessmpt  46376  sge0iunmptlemfi  46390  sge0iunmptlemre  46392  sge0iunmpt  46395  sge0rpcpnf  46398  sge0isum  46404  nnfoctbdjlem  46432  psmeasure  46448  voliunsge0lem  46449  meaiuninclem  46457  meaiuninc3v  46461  meaiininclem  46463  omeiunltfirp  46496  carageniuncllem2  46499  caratheodorylem1  46503  caratheodorylem2  46504  isomenndlem  46507  hoicvr  46525  hoicvrrex  46533  ovnsupge0  46534  ovnlecvr  46535  ovnf  46540  ovn0lem  46542  ovnsubaddlem1  46547  ovnsubadd  46549  hsphoif  46553  sge0hsphoire  46566  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmv1lelem3  46570  hoidmv1le  46571  hoidmvlelem2  46573  hoidmvlelem3  46574  ovnhoilem1  46578  ovnsubadd2lem  46622  ovolval4lem1  46626  ovolval4lem2  46627  ovolval5lem2  46630  ovnovollem1  46633  ovnovollem2  46634  vonioolem2  46658  vonicclem2  46661  smflim  46754  nsssmfmbflem  46755  smfmullem4  46771  smfsuplem1  46788  smfsuplem3  46790  smflimsuplem3  46799  fsetsnf  47028  cfsetsnfsetf  47035  cfsetsnfsetfo  47037  imasetpreimafvbijlemf  47363  prproropf1o  47469  fmtnodvds  47506  upgrimwlklem2  47859  isubgr3stgrlem6  47931  lincvalsc0  48345  lcoc0  48346  linc0scn0  48347  linc1  48349  lincscm  48354  lincresunit3  48405  1arympt1  48566  1arymaptf  48569  2arympt  48577  2arymaptf  48580  ackendofnn0  48612  amgmlemALT  49615