MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fmpti Structured version   Unicode version

Theorem fmpti 6060
Description: Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
Hypotheses
Ref Expression
fmpt.1  |-  F  =  ( x  e.  A  |->  C )
fmpti.2  |-  ( x  e.  A  ->  C  e.  B )
Assertion
Ref Expression
fmpti  |-  F : A
--> B
Distinct variable groups:    x, A    x, B
Allowed substitution hints:    C( x)    F( x)

Proof of Theorem fmpti
StepHypRef Expression
1 fmpti.2 . . 3  |-  ( x  e.  A  ->  C  e.  B )
21rgen 2781 . 2  |-  A. x  e.  A  C  e.  B
3 fmpt.1 . . 3  |-  F  =  ( x  e.  A  |->  C )
43fmpt 6058 . 2  |-  ( A. x  e.  A  C  e.  B  <->  F : A --> B )
52, 4mpbi 211 1  |-  F : A
--> B
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1872   A.wral 2771    |-> cmpt 4482   -->wf 5597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609
This theorem is referenced by:  harf  8084  r0weon  8451  dfac2a  8567  ackbij1lem10  8666  cff  8685  isf32lem9  8798  fin1a2lem2  8838  fin1a2lem4  8840  facmapnn  12476  ccatfnOLD  12722  wwlktovf  13031  cjf  13167  ref  13175  imf  13176  absf  13400  limsupcl  13528  limsupclOLD  13529  limsupgf  13532  eff  14135  sinf  14177  cosf  14178  bitsf  14399  fnum  14690  fden  14691  lcmsmapnnOLD  15010  prmormapnnOLD  15013  prmgapprmo  15032  setcepi  15982  catcfuccl  16003  staffval  18074  ocvfval  19227  pjfval  19267  pjpm  19269  leordtval2  20226  lecldbas  20233  nmfval  21601  nmoffn  21714  nmofval  21717  nmoffnOLD  21735  nmofvalOLD  21736  divcn  21898  xrhmeo  21972  tchex  22189  tchnmfval  22200  ioorf  22523  ioorfOLD  22528  dveflem  22929  resinf1o  23483  efifo  23494  logcnlem5  23589  resqrtcn  23687  asinf  23796  acosf  23798  atanf  23804  leibpilem2  23865  areaf  23885  emcllem1  23919  igamf  23974  chtf  24033  chpf  24048  ppif  24055  muf  24065  bposlem7  24216  pntrf  24399  pntrsumo1  24401  pntsf  24409  pntrlog2bndlem4  24416  pntrlog2bndlem5  24417  normf  26774  hosubcli  27420  cnlnadjlem4  27721  cnlnadjlem6  27723  eulerpartlemsf  29200  fiblem  29239  signsvvf  29476  derangf  29899  snmlff  30060  sinccvglem  30324  circum  30326  f1omptsnlem  31702  phpreu  31893  poimirlem26  31930  cncfres  32061  lsatset  32525  lhe4.4ex1a  36648  clim1fr1  37619  dvsinax  37723  wallispilem5  37871  wallispi  37872  stirlinglem5  37880  stirlinglem13  37888  stirlinglem14  37889  stirlinglem15  37890  stirlingr  37892  fourierdlem43  37954  fourierdlem57  37967  fourierdlem58  37968  fourierdlem62  37972  fouriersw  38035  0ome  38258
  Copyright terms: Public domain W3C validator