Theorem fmptd 7107

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 7103	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶)
5	2, 4	sylib 221	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076   ↦ cmpt 5186  ⟶wf 6529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-fun 6535  df-fn 6536  df-f 6537

This theorem is used by:  fmpttd  7108  fnwelem  8129  fsetfcdm  8861  fdiagfn  8897  resixpfo  8943  xpmapenlem  9142  unxpdomlem3  9228  fsuppmptdm  9346  cantnfp1lem1  9657  cantnfp1lem2  9658  cantnfp1lem3  9659  cantnf  9672  updjudhf  9936  fseqenlem2  10028  dfac8clem  10035  coftr  10275  isf34lem2  10375  axcc2lem  10438  axdc2lem  10450  axdc3lem4  10455  pwcfsdom  10592  rpnnen1lem1  13028  tpf  14564  caucvg  15766  sumrblem  15797  summolem2a  15801  supcvg  15945  prodrblem  16016  prodmolem2a  16021  crth  16869  eulerthlem1  16872  prmreclem6  17013  4sqlem11  17047  vdwlem2  17074  vdwlem4  17076  vdwlem6  17078  vdwlem10  17082  ramub1lem2  17119  prmgaplcm  17152  frmdup1  18973  grpinvf  19110  mulgnngsum  19202  cycsubm  19330  cycsubgcl  19334  cycsubgss  19335  conjghm  19376  conjnmz  19379  qusghm  19382  galactghm  19531  symgextf  19544  symgfixf  19563  pmtrdifwrdellem1  19608  odf1  19689  dfod2  19691  pgpssslw  19741  frgpmhm  19892  gsummptfidmsplitres  20058  gsummptfidminv  20074  gsumzunsnd  20083  gsummpt1n0  20092  ablfac1b  20199  ablfac2  20218  c0mgm  20600  c0mhm  20601  c0snmgmhm  20603  abvtrivd  20998  issrngd  21021  pwssplit0  21242  rngqiprngimf  21500  mulgghm2  21689  frobrhm  21788  isphld  21867  pjff  21925  frlmup1  22011  asclf  22096  psr1cl  22175  evlslem1  22298  evlsval2  22303  evlsval3  22305  mplmapghm  22338  evlsmaprhm  22347  selvcllem5  22355  evls1maprhm  22601  rhmmpl  22605  scmatf  22751  mdetf  22817  maduf  22863  pmatcollpw3fi1lem1  23011  chfacfisf  23079  chfacfisfcpmat  23080  cpmidpmatlem2  23096  lly1stc  23722  txcnmpt  23850  txlm  23874  xkoinjcn  23913  kqffn  23951  txflf  24232  tsmsfbas  24354  ustuqtop0  24466  metdsf  25075  metdsge  25076  mulc1cncf  25133  lebnumlem1  25189  cmetcaulem  25516  ovollb2lem  25716  ovolctb  25718  ovolunlem1a  25724  ovolunlem1  25725  ovoliunlem1  25730  ovoliunlem2  25731  ovoliun  25733  ovolshftlem1  25737  ovolscalem1  25741  ovolicc1  25744  ioombl1lem1  25786  uniioombllem2  25811  volsup2  25833  volcn  25834  vitalilem4  25839  vitalilem5  25840  mbfconst  25861  mbfmax  25877  mbfsup  25892  i1f1lem  25917  i1f1  25918  i1fres  25933  itg1climres  25942  itg2splitlem  25976  itg2split  25977  itg2monolem1  25978  itg2mono  25981  itg2i1fseq  25983  itg2i1fseq2  25984  dvreslem  26136  dvmptresicc  26143  dvivthlem1  26235  dvfsumrlimf  26252  dvfsumlem3  26255  ftc1lem2  26263  ftc1lem6  26268  radcnvlem1  26649  pserulm  26658  psercn2  26659  abelthlem4  26670  efif1olem4  26782  lgamgulmlem6  27270  gamcvg  27292  basellem4  27320  basellem7  27323  basellem9  27325  lgsfcl2  27539  lgsqrlem2  27583  lgseisenlem1  27611  dchrmusum2  27730  dchrvmasumiflem1  27737  dchrisum0ff  27743  dchrisum0lem1b  27751  dchrisum0lem2a  27753  abvcxp  27851  padicabv  27866  axlowdimlem15  29413  crctcshwlkn0  30289  wlkiswwlks2lem5  30341  wlkswwlksf1o  30347  wwlksnextfun  30366  clwlkclwwlklem2a  30468  clwlkclwwlkf  30478  clwwlkf  30517  frgrncvvdeqlem4  30782  numclwwlk1lem2f  30835  numclwlk2lem2f  30857  ipblnfi  31336  ubthlem1  31351  htthlem  31398  hlimadd  31674  chscllem1  32118  cnlnadjlem2  32549  strlem3a  32733  hstrlem3a  32741  xppreima2  33124  suppovss  33153  fsuppcurry1  33195  fsuppcurry2  33196  pwrssmgc  33440  mndlactf1  33466  mndlactfo  33467  mndractf1  33468  mndractfo  33469  lmodvslmhm  33490  conjga  33610  rlocf1  33714  nsgmgc  33841  elrspunidl  33856  r1plmhm  34019  r1pquslmic  34020  selvply1rhmlem1  34030  mplvrpmga  34055  mplvrpmmhm  34056  mplvrpmrhm  34057  psrmonprod  34062  mplmonprod  34064  ply1degltdimlem  34132  ply1degltdim  34133  extdgfialglem1  34202  algextdeglem8  34234  rhmpreimacnlem  34394  rhmpreimacn  34395  xrge0mulc1cn  34451  esumpcvgval  34588  esumcvg  34596  mbfmco2  34776  eulerpartlems  34871  onvfowev  35713  erdszelem9  35778  cvmlift3lem3  35900  ex-sategoelel  36000  ex-sategoelelomsuc  36005  elmrsubrn  36099  mvhf  36137  iprodefisum  36320  unbdqndv1  37205  knoppf  37232  ftc1anclem3  38444  ftc1anclem5  38446  lflnegcl  39948  lshpkrcl  39989  tendo0cl  41663  primrootscoprf  42967  aks6d1c2p1  42984  aks6d1c4  42990  aks6d1c2lem4  42993  aks6d1c2  42996  aks6d1c5lem0  43001  aks6d1c5  43005  sticksstones2  43013  sticksstones8  43019  sticksstones9  43020  sticksstones10  43021  sticksstones11  43022  sticksstones12a  43023  sticksstones17  43029  sticksstones18  43030  aks6d1c6lem2  43037  aks6d1c6lem3  43038  aks6d1c6lem4  43039  aks6d1c6isolem1  43040  aks6d1c6isolem2  43041  aks6d1c6isolem3  43042  aks6d1c6lem5  43043  aks5lem2  43053  frlmsnic  43422  rhmpsr  43429  evlsbagval  43432  cantnfub  44162  binomcxplemradcnv  45176  binomcxplemcvg  45178  binomcxplemnotnn0  45180  projf1o  46028  mullimc  46446  ellimcabssub0  46447  mullimcf  46453  constlimc  46454  idlimc  46456  neglimc  46475  addlimc  46476  0ellimcdiv  46477  fnlimf  46506  liminfpnfuz  46644  xlimpnfxnegmnf2  46686  cncfshift  46702  icccncfext  46715  cncfiooiccre  46723  fprodsubrecnncnvlem  46735  fprodaddrecnncnvlem  46737  ioodvbdlimc1lem1  46759  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  dvnxpaek  46770  dvnprodlem1  46774  itgsinexplem1  46782  itgiccshift  46808  dirkercncflem2  46932  fourierdlem4  46939  fourierdlem5  46940  fourierdlem9  46944  fourierdlem14  46949  fourierdlem16  46951  fourierdlem17  46952  fourierdlem18  46953  fourierdlem21  46956  fourierdlem22  46957  fourierdlem37  46972  fourierdlem50  46984  fourierdlem51  46985  fourierdlem53  46987  fourierdlem55  46989  fourierdlem57  46991  fourierdlem58  46992  fourierdlem59  46993  fourierdlem60  46994  fourierdlem61  46995  fourierdlem67  47001  fourierdlem68  47002  fourierdlem72  47006  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem76  47010  fourierdlem78  47012  fourierdlem80  47014  fourierdlem81  47015  fourierdlem83  47017  fourierdlem84  47018  fourierdlem88  47022  fourierdlem92  47026  fourierdlem93  47027  fourierdlem97  47031  fourierdlem101  47035  fourierdlem103  47037  fourierdlem104  47038  fourierdlem111  47045  sqwvfoura  47056  elaa2lem  47061  etransclem1  47063  etransclem8  47070  etransclem20  47082  etransclem33  47095  etransclem35  47097  etransclem39  47101  rrxtopnfi  47115  ioorrnopnxrlem  47134  sge0tsms  47208  sge0snmpt  47211  sge0fsummpt  47218  sge0pr  47222  sge0lessmpt  47227  sge0iunmptlemfi  47241  sge0iunmptlemre  47243  sge0iunmpt  47246  sge0rpcpnf  47249  sge0isum  47255  nnfoctbdjlem  47283  psmeasure  47299  voliunsge0lem  47300  meaiuninclem  47308  meaiuninc3v  47312  meaiininclem  47314  omeiunltfirp  47347  carageniuncllem2  47350  caratheodorylem1  47354  caratheodorylem2  47355  isomenndlem  47358  hoicvrrex  47384  ovnsupge0  47385  ovnlecvr  47386  ovnf  47391  ovn0lem  47393  ovnsubaddlem1  47398  ovnsubadd  47400  hsphoif  47404  sge0hsphoire  47417  hoidmv1lelem1  47419  hoidmv1lelem2  47420  hoidmv1lelem3  47421  hoidmv1le  47422  hoidmvlelem2  47424  hoidmvlelem3  47425  ovnhoilem1  47429  ovnsubadd2lem  47473  ovolval4lem1  47477  ovolval4lem2  47478  ovolval5lem2  47481  ovnovollem1  47484  ovnovollem2  47485  vonioolem2  47509  vonicclem2  47512  smflim  47605  nsssmfmbflem  47606  smfmullem4  47622  smfsuplem1  47639  smfsuplem3  47641  smflimsuplem3  47650  fsetsnf  47939  cfsetsnfsetf  47946  cfsetsnfsetfo  47948  imasetpreimafvbijlemf  48301  prproropf1o  48407  fmtnodvds  48447  upgrimwlklem2  48814  isubgr3stgrlem6  48887  lincvalsc0  49351  lcoc0  49352  linc0scn0  49353  linc1  49355  lincscm  49360  lincresunit3  49411  1arympt1  49568  1arymaptf  49571  2arympt  49579  2arymaptf  49582  ackendofnn0  49614  amgmlemALT  50821