Theorem fmptd 7112

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

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

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 2733  ax-sep 5249  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  fmpttd  7113  fnwelem  8141  fsetfcdm  8875  fdiagfn  8911  resixpfo  8957  xpmapenlem  9156  unxpdomlem3  9242  fsuppmptdm  9361  cantnfp1lem1  9672  cantnfp1lem2  9673  cantnfp1lem3  9674  cantnf  9687  updjudhf  10005  fseqenlem2  10097  dfac8clem  10104  coftr  10344  isf34lem2  10444  axcc2lem  10507  axdc2lem  10519  axdc3lem4  10524  pwcfsdom  10661  rpnnen1lem1  13099  tpf  14637  caucvg  15839  sumrblem  15870  summolem2a  15874  supcvg  16018  prodrblem  16089  prodmolem2a  16094  crth  16948  eulerthlem1  16951  prmreclem6  17092  4sqlem11  17126  vdwlem2  17153  vdwlem4  17155  vdwlem6  17157  vdwlem10  17161  ramub1lem2  17198  prmgaplcm  17231  frmdup1  19053  grpinvf  19190  mulgnngsum  19282  cycsubm  19410  cycsubgcl  19414  cycsubgss  19415  conjghm  19456  conjnmz  19459  qusghm  19462  galactghm  19611  symgextf  19624  symgfixf  19643  pmtrdifwrdellem1  19688  odf1  19769  dfod2  19771  pgpssslw  19821  frgpmhm  19972  gsummptfidmsplitres  20138  gsummptfidminv  20154  gsumzunsnd  20163  gsummpt1n0  20172  ablfac1b  20279  ablfac2  20298  c0mgm  20682  c0mhm  20683  c0snmgmhm  20685  abvtrivd  21082  issrngd  21105  pwssplit0  21326  rngqiprngimf  21586  mulgghm2  21775  frobrhm  21874  isphld  21953  pjff  22011  frlmup1  22097  asclf  22182  psr1cl  22261  evlslem1  22384  evlsval2  22389  evlsval3  22391  mplmapghm  22424  evlsmaprhm  22433  selvcllem5  22441  evls1maprhm  22687  rhmmpl  22691  scmatf  22837  mdetf  22903  maduf  22949  pmatcollpw3fi1lem1  23097  chfacfisf  23165  chfacfisfcpmat  23166  cpmidpmatlem2  23182  lly1stc  23808  txcnmpt  23936  txlm  23960  xkoinjcn  23999  kqffn  24037  txflf  24318  tsmsfbas  24440  ustuqtop0  24552  metdsf  25161  metdsge  25162  mulc1cncf  25219  lebnumlem1  25275  cmetcaulem  25602  ovollb2lem  25802  ovolctb  25804  ovolunlem1a  25810  ovolunlem1  25811  ovoliunlem1  25816  ovoliunlem2  25817  ovoliun  25819  ovolshftlem1  25823  ovolscalem1  25827  ovolicc1  25830  ioombl1lem1  25872  uniioombllem2  25897  volsup2  25919  volcn  25920  vitalilem4  25925  vitalilem5  25926  mbfconst  25947  mbfmax  25963  mbfsup  25978  i1f1lem  26003  i1f1  26004  i1fres  26019  itg1climres  26028  itg2splitlem  26062  itg2split  26063  itg2monolem1  26064  itg2mono  26067  itg2i1fseq  26069  itg2i1fseq2  26070  dvreslem  26222  dvmptresicc  26229  dvivthlem1  26321  dvfsumrlimf  26338  dvfsumlem3  26341  ftc1lem2  26349  ftc1lem6  26354  radcnvlem1  26733  pserulm  26742  psercn2  26743  abelthlem4  26754  efif1olem4  26866  lgamgulmlem6  27354  gamcvg  27376  basellem4  27404  basellem7  27407  basellem9  27409  lgsfcl2  27623  lgsqrlem2  27667  lgseisenlem1  27695  dchrmusum2  27814  dchrvmasumiflem1  27821  dchrisum0ff  27827  dchrisum0lem1b  27835  dchrisum0lem2a  27837  abvcxp  27935  padicabv  27950  axlowdimlem15  29527  crctcshwlkn0  30403  wlkiswwlks2lem5  30455  wlkswwlksf1o  30461  wwlksnextfun  30480  clwlkclwwlklem2a  30582  clwlkclwwlkf  30592  clwwlkf  30631  frgrncvvdeqlem4  30896  numclwwlk1lem2f  30949  numclwlk2lem2f  30971  ipblnfi  31450  ubthlem1  31465  htthlem  31512  hlimadd  31788  chscllem1  32232  cnlnadjlem2  32663  strlem3a  32847  hstrlem3a  32855  xppreima2  33238  suppovss  33267  fsuppcurry1  33309  fsuppcurry2  33310  pwrssmgc  33554  mndlactf1  33580  mndlactfo  33581  mndractf1  33582  mndractfo  33583  lmodvslmhm  33604  conjga  33724  rlocf1  33828  nsgmgc  33956  elrspunidl  33971  r1plmhm  34134  r1pquslmic  34135  selvply1rhmlem1  34145  mplvrpmga  34170  mplvrpmmhm  34171  mplvrpmrhm  34172  psrmonprod  34177  mplmonprod  34179  ply1degltdimlem  34247  ply1degltdim  34248  extdgfialglem1  34317  algextdeglem8  34349  rhmpreimacnlem  34509  rhmpreimacn  34510  xrge0mulc1cn  34566  esumpcvgval  34703  esumcvg  34711  mbfmco2  34890  eulerpartlems  34985  onvfowev  35878  erdszelem9  35943  cvmlift3lem3  36065  ex-sategoelel  36165  ex-sategoelelomsuc  36170  elmrsubrn  36264  mvhf  36302  iprodefisum  36485  unbdqndv1  37354  knoppf  37381  ftc1anclem3  38593  ftc1anclem5  38595  lflnegcl  40112  lshpkrcl  40153  tendo0cl  41827  primrootscoprf  43131  aks6d1c2p1  43148  aks6d1c4  43154  aks6d1c2lem4  43157  aks6d1c2  43160  aks6d1c5lem0  43165  aks6d1c5  43169  sticksstones2  43177  sticksstones8  43183  sticksstones9  43184  sticksstones10  43185  sticksstones11  43186  sticksstones12a  43187  sticksstones17  43193  sticksstones18  43194  aks6d1c6lem2  43201  aks6d1c6lem3  43202  aks6d1c6lem4  43203  aks6d1c6isolem1  43204  aks6d1c6isolem2  43205  aks6d1c6isolem3  43206  aks6d1c6lem5  43207  aks5lem2  43217  frlmsnic  43584  rhmpsr  43591  evlsbagval  43594  cantnfub  44307  binomcxplemradcnv  45321  binomcxplemcvg  45323  binomcxplemnotnn0  45325  projf1o  46180  mullimc  46597  ellimcabssub0  46598  mullimcf  46604  constlimc  46605  idlimc  46607  neglimc  46626  addlimc  46627  0ellimcdiv  46628  fnlimf  46657  liminfpnfuz  46795  xlimpnfxnegmnf2  46837  cncfshift  46853  icccncfext  46866  cncfiooiccre  46874  fprodsubrecnncnvlem  46886  fprodaddrecnncnvlem  46888  ioodvbdlimc1lem1  46910  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvnxpaek  46921  dvnprodlem1  46925  itgsinexplem1  46933  itgiccshift  46959  dirkercncflem2  47083  fourierdlem4  47090  fourierdlem5  47091  fourierdlem9  47095  fourierdlem14  47100  fourierdlem16  47102  fourierdlem17  47103  fourierdlem18  47104  fourierdlem21  47107  fourierdlem22  47108  fourierdlem37  47123  fourierdlem50  47135  fourierdlem51  47136  fourierdlem53  47138  fourierdlem55  47140  fourierdlem57  47142  fourierdlem58  47143  fourierdlem59  47144  fourierdlem60  47145  fourierdlem61  47146  fourierdlem67  47152  fourierdlem68  47153  fourierdlem72  47157  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem76  47161  fourierdlem78  47163  fourierdlem80  47165  fourierdlem81  47166  fourierdlem83  47168  fourierdlem84  47169  fourierdlem88  47173  fourierdlem92  47177  fourierdlem93  47178  fourierdlem97  47182  fourierdlem101  47186  fourierdlem103  47188  fourierdlem104  47189  fourierdlem111  47196  sqwvfoura  47207  elaa2lem  47212  etransclem1  47214  etransclem8  47221  etransclem20  47233  etransclem33  47246  etransclem35  47248  etransclem39  47252  rrxtopnfi  47266  ioorrnopnxrlem  47285  sge0tsms  47359  sge0snmpt  47362  sge0fsummpt  47369  sge0pr  47373  sge0lessmpt  47378  sge0iunmptlemfi  47392  sge0iunmptlemre  47394  sge0iunmpt  47397  sge0rpcpnf  47400  sge0isum  47406  nnfoctbdjlem  47434  psmeasure  47450  voliunsge0lem  47451  meaiuninclem  47459  meaiuninc3v  47463  meaiininclem  47465  omeiunltfirp  47498  carageniuncllem2  47501  caratheodorylem1  47505  caratheodorylem2  47506  isomenndlem  47509  hoicvrrex  47535  ovnsupge0  47536  ovnlecvr  47537  ovnf  47542  ovn0lem  47544  ovnsubaddlem1  47549  ovnsubadd  47551  hsphoif  47555  sge0hsphoire  47568  hoidmv1lelem1  47570  hoidmv1lelem2  47571  hoidmv1lelem3  47572  hoidmv1le  47573  hoidmvlelem2  47575  hoidmvlelem3  47576  ovnhoilem1  47580  ovnsubadd2lem  47624  ovolval4lem1  47628  ovolval4lem2  47629  ovolval5lem2  47632  ovnovollem1  47635  ovnovollem2  47636  vonioolem2  47660  vonicclem2  47663  smflim  47756  nsssmfmbflem  47757  smfmullem4  47773  smfsuplem1  47790  smfsuplem3  47792  smflimsuplem3  47801  fsetsnf  48090  cfsetsnfsetf  48097  cfsetsnfsetfo  48099  imasetpreimafvbijlemf  48452  prproropf1o  48558  fmtnodvds  48598  upgrimwlklem2  48965  isubgr3stgrlem6  49038  lincvalsc0  49502  lcoc0  49503  linc0scn0  49504  linc1  49506  lincscm  49511  lincresunit3  49562  1arympt1  49719  1arymaptf  49722  2arympt  49730  2arymaptf  49733  ackendofnn0  49765  amgmlemALT  50957