Theorem fmptd 7114

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076   ↦ cmpt 5185  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-fun 6540  df-fn 6541  df-f 6542

This theorem is used by:  fmpttd  7115  fnwelem  8143  fsetfcdm  8883  fdiagfn  8919  resixpfo  8965  xpmapenlem  9164  unxpdomlem3  9250  fsuppmptdm  9369  cantnfp1lem1  9680  cantnfp1lem2  9681  cantnfp1lem3  9682  cantnf  9695  updjudhf  10013  fseqenlem2  10105  dfac8clem  10112  coftr  10352  isf34lem2  10452  axcc2lem  10515  axdc2lem  10527  axdc3lem4  10532  pwcfsdom  10669  rpnnen1lem1  13107  tpf  14645  caucvg  15847  sumrblem  15878  summolem2a  15882  supcvg  16026  prodrblem  16097  prodmolem2a  16102  crth  16956  eulerthlem1  16959  prmreclem6  17100  4sqlem11  17134  vdwlem2  17161  vdwlem4  17163  vdwlem6  17165  vdwlem10  17169  ramub1lem2  17206  prmgaplcm  17239  frmdup1  19061  grpinvf  19198  mulgnngsum  19290  cycsubm  19418  cycsubgcl  19422  cycsubgss  19423  conjghm  19464  conjnmz  19467  qusghm  19470  galactghm  19619  symgextf  19632  symgfixf  19651  pmtrdifwrdellem1  19696  odf1  19777  dfod2  19779  pgpssslw  19829  frgpmhm  19980  gsummptfidmsplitres  20146  gsummptfidminv  20162  gsumzunsnd  20171  gsummpt1n0  20180  ablfac1b  20287  ablfac2  20306  c0mgm  20690  c0mhm  20691  c0snmgmhm  20693  abvtrivd  21090  issrngd  21113  pwssplit0  21334  rngqiprngimf  21594  mulgghm2  21783  frobrhm  21882  isphld  21961  pjff  22019  frlmup1  22105  asclf  22190  psr1cl  22269  evlslem1  22392  evlsval2  22397  evlsval3  22399  mplmapghm  22432  evlsmaprhm  22441  selvcllem5  22449  evls1maprhm  22695  rhmmpl  22699  scmatf  22845  mdetf  22911  maduf  22957  pmatcollpw3fi1lem1  23105  chfacfisf  23173  chfacfisfcpmat  23174  cpmidpmatlem2  23190  lly1stc  23816  txcnmpt  23944  txlm  23968  xkoinjcn  24007  kqffn  24045  txflf  24326  tsmsfbas  24448  ustuqtop0  24560  metdsf  25169  metdsge  25170  mulc1cncf  25227  lebnumlem1  25283  cmetcaulem  25610  ovollb2lem  25810  ovolctb  25812  ovolunlem1a  25818  ovolunlem1  25819  ovoliunlem1  25824  ovoliunlem2  25825  ovoliun  25827  ovolshftlem1  25831  ovolscalem1  25835  ovolicc1  25838  ioombl1lem1  25880  uniioombllem2  25905  volsup2  25927  volcn  25928  vitalilem4  25933  vitalilem5  25934  mbfconst  25955  mbfmax  25971  mbfsup  25986  i1f1lem  26011  i1f1  26012  i1fres  26027  itg1climres  26036  itg2splitlem  26070  itg2split  26071  itg2monolem1  26072  itg2mono  26075  itg2i1fseq  26077  itg2i1fseq2  26078  dvreslem  26230  dvmptresicc  26237  dvivthlem1  26329  dvfsumrlimf  26346  dvfsumlem3  26349  ftc1lem2  26357  ftc1lem6  26362  radcnvlem1  26741  pserulm  26750  psercn2  26751  abelthlem4  26762  efif1olem4  26874  lgamgulmlem6  27362  gamcvg  27384  basellem4  27412  basellem7  27415  basellem9  27417  lgsfcl2  27631  lgsqrlem2  27675  lgseisenlem1  27703  dchrmusum2  27822  dchrvmasumiflem1  27829  dchrisum0ff  27835  dchrisum0lem1b  27843  dchrisum0lem2a  27845  abvcxp  27943  padicabv  27958  axlowdimlem15  29535  crctcshwlkn0  30411  wlkiswwlks2lem5  30463  wlkswwlksf1o  30469  wwlksnextfun  30488  clwlkclwwlklem2a  30590  clwlkclwwlkf  30600  clwwlkf  30639  frgrncvvdeqlem4  30904  numclwwlk1lem2f  30957  numclwlk2lem2f  30979  ipblnfi  31458  ubthlem1  31473  htthlem  31520  hlimadd  31796  chscllem1  32240  cnlnadjlem2  32671  strlem3a  32855  hstrlem3a  32863  xppreima2  33288  suppovss  33317  fsuppcurry1  33359  fsuppcurry2  33360  pwrssmgc  33604  mndlactf1  33630  mndlactfo  33631  mndractf1  33632  mndractfo  33633  lmodvslmhm  33654  conjga  33774  rlocf1  33878  nsgmgc  34006  elrspunidl  34021  r1plmhm  34184  r1pquslmic  34185  selvply1rhmlem1  34195  mplvrpmga  34220  mplvrpmmhm  34221  mplvrpmrhm  34222  psrmonprod  34227  mplmonprod  34229  ply1degltdimlem  34297  ply1degltdim  34298  extdgfialglem1  34367  algextdeglem8  34399  rhmpreimacnlem  34559  rhmpreimacn  34560  xrge0mulc1cn  34616  esumpcvgval  34753  esumcvg  34761  mbfmco2  34940  eulerpartlems  35035  onvfowev  35942  erdszelem9  36007  cvmlift3lem3  36129  ex-sategoelel  36229  ex-sategoelelomsuc  36234  elmrsubrn  36328  mvhf  36366  iprodefisum  36549  unbdqndv1  37417  knoppf  37444  ftc1anclem3  38657  ftc1anclem5  38659  lflnegcl  40176  lshpkrcl  40217  tendo0cl  41891  primrootscoprf  43195  aks6d1c2p1  43212  aks6d1c4  43218  aks6d1c2lem4  43221  aks6d1c2  43224  aks6d1c5lem0  43229  aks6d1c5  43233  sticksstones2  43241  sticksstones8  43247  sticksstones9  43248  sticksstones10  43249  sticksstones11  43250  sticksstones12a  43251  sticksstones17  43257  sticksstones18  43258  aks6d1c6lem2  43265  aks6d1c6lem3  43266  aks6d1c6lem4  43267  aks6d1c6isolem1  43268  aks6d1c6isolem2  43269  aks6d1c6isolem3  43270  aks6d1c6lem5  43271  aks5lem2  43281  frlmsnic  43648  rhmpsr  43655  evlsbagval  43658  cantnfub  44367  binomcxplemradcnv  45380  binomcxplemcvg  45382  binomcxplemnotnn0  45384  projf1o  46255  mullimc  46672  ellimcabssub0  46673  mullimcf  46679  constlimc  46680  idlimc  46682  neglimc  46701  addlimc  46702  0ellimcdiv  46703  fnlimf  46732  liminfpnfuz  46870  xlimpnfxnegmnf2  46912  cncfshift  46928  icccncfext  46941  cncfiooiccre  46949  fprodsubrecnncnvlem  46961  fprodaddrecnncnvlem  46963  ioodvbdlimc1lem1  46985  ioodvbdlimc1lem2  46986  ioodvbdlimc2lem  46988  dvnxpaek  46996  dvnprodlem1  47000  itgsinexplem1  47008  itgiccshift  47034  dirkercncflem2  47158  fourierdlem4  47165  fourierdlem5  47166  fourierdlem9  47170  fourierdlem14  47175  fourierdlem16  47177  fourierdlem17  47178  fourierdlem18  47179  fourierdlem21  47182  fourierdlem22  47183  fourierdlem37  47198  fourierdlem50  47210  fourierdlem51  47211  fourierdlem53  47213  fourierdlem55  47215  fourierdlem57  47217  fourierdlem58  47218  fourierdlem59  47219  fourierdlem60  47220  fourierdlem61  47221  fourierdlem67  47227  fourierdlem68  47228  fourierdlem72  47232  fourierdlem73  47233  fourierdlem74  47234  fourierdlem75  47235  fourierdlem76  47236  fourierdlem78  47238  fourierdlem80  47240  fourierdlem81  47241  fourierdlem83  47243  fourierdlem84  47244  fourierdlem88  47248  fourierdlem92  47252  fourierdlem93  47253  fourierdlem97  47257  fourierdlem101  47261  fourierdlem103  47263  fourierdlem104  47264  fourierdlem111  47271  sqwvfoura  47282  elaa2lem  47287  etransclem1  47289  etransclem8  47296  etransclem20  47308  etransclem33  47321  etransclem35  47323  etransclem39  47327  rrxtopnfi  47341  ioorrnopnxrlem  47360  sge0tsms  47434  sge0snmpt  47437  sge0fsummpt  47444  sge0pr  47448  sge0lessmpt  47453  sge0iunmptlemfi  47467  sge0iunmptlemre  47469  sge0iunmpt  47472  sge0rpcpnf  47475  sge0isum  47481  nnfoctbdjlem  47509  psmeasure  47525  voliunsge0lem  47526  meaiuninclem  47534  meaiuninc3v  47538  meaiininclem  47540  omeiunltfirp  47573  carageniuncllem2  47576  caratheodorylem1  47580  caratheodorylem2  47581  isomenndlem  47584  hoicvrrex  47610  ovnsupge0  47611  ovnlecvr  47612  ovnf  47617  ovn0lem  47619  ovnsubaddlem1  47624  ovnsubadd  47626  hsphoif  47630  sge0hsphoire  47643  hoidmv1lelem1  47645  hoidmv1lelem2  47646  hoidmv1lelem3  47647  hoidmv1le  47648  hoidmvlelem2  47650  hoidmvlelem3  47651  ovnhoilem1  47655  ovnsubadd2lem  47699  ovolval4lem1  47703  ovolval4lem2  47704  ovolval5lem2  47707  ovnovollem1  47710  ovnovollem2  47711  vonioolem2  47735  vonicclem2  47738  smflim  47831  nsssmfmbflem  47832  smfmullem4  47848  smfsuplem1  47865  smfsuplem3  47867  smflimsuplem3  47876  fsetsnf  48165  cfsetsnfsetf  48172  cfsetsnfsetfo  48174  imasetpreimafvbijlemf  48527  prproropf1o  48633  fmtnodvds  48673  upgrimwlklem2  49040  isubgr3stgrlem6  49113  lincvalsc0  49577  lcoc0  49578  linc0scn0  49579  linc1  49581  lincscm  49586  lincresunit3  49637  1arympt1  49794  1arymaptf  49797  2arympt  49805  2arymaptf  49808  ackendofnn0  49840  amgmlemALT  51032