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

Theorem fmpti 6034
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 2766 . 2  |-  A. x  e.  A  C  e.  B
3 fmpt.1 . . 3  |-  F  =  ( x  e.  A  |->  C )
43fmpt 6032 . 2  |-  ( A. x  e.  A  C  e.  B  <->  F : A --> B )
52, 4mpbi 210 1  |-  F : A
--> B
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1407    e. wcel 1844   A.wral 2756    |-> cmpt 4455   -->wf 5567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-sep 4519  ax-nul 4527  ax-pr 4632
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3063  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981  df-uni 4194  df-br 4398  df-opab 4456  df-mpt 4457  df-id 4740  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-fv 5579
This theorem is referenced by:  harf  8022  r0weon  8424  dfac2a  8544  ackbij1lem10  8643  cff  8662  isf32lem9  8775  fin1a2lem2  8815  fin1a2lem4  8817  ccatfnOLD  12647  wwlktovf  12952  cjf  13088  ref  13096  imf  13097  absf  13321  limsupcl  13447  limsupgf  13449  eff  14028  sinf  14070  cosf  14071  bitsf  14288  fnum  14486  fden  14487  setcepi  15693  catcfuccl  15714  staffval  17818  ocvfval  18997  pjfval  19037  pjpm  19039  leordtval2  20008  lecldbas  20015  nmfval  21403  nmoffn  21512  nmofval  21515  divcn  21666  xrhmeo  21740  tchex  21954  tchnmfval  21965  ioorf  22276  dveflem  22674  resinf1o  23217  efifo  23228  logcnlem5  23323  resqrtcn  23421  asinf  23530  acosf  23532  atanf  23538  leibpilem2  23599  areaf  23619  emcllem1  23653  igamf  23708  chtf  23765  chpf  23780  ppif  23787  muf  23797  bposlem7  23948  pntrf  24131  pntrsumo1  24133  pntsf  24141  pntrlog2bndlem4  24148  pntrlog2bndlem5  24149  normf  26467  hosubcli  27114  cnlnadjlem4  27415  cnlnadjlem6  27417  eulerpartlemsf  28817  fiblem  28856  signsvvf  29055  derangf  29478  snmlff  29639  sinccvglem  29903  circum  29905  f1omptsnlem  31265  cncfres  31556  lsatset  32021  lhe4.4ex1a  36095  clim1fr1  36988  dvsinax  37089  wallispilem5  37232  wallispi  37233  stirlinglem5  37241  stirlinglem13  37249  stirlinglem14  37250  stirlinglem15  37251  stirlingr  37253  fourierdlem43  37313  fourierdlem57  37327  fourierdlem58  37328  fourierdlem62  37332  fouriersw  37395
  Copyright terms: Public domain W3C validator