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

Theorem fmpti 5894
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 2773 . 2  |-  A. x  e.  A  C  e.  B
3 fmpt.1 . . 3  |-  F  =  ( x  e.  A  |->  C )
43fmpt 5892 . 2  |-  ( A. x  e.  A  C  e.  B  <->  F : A --> B )
52, 4mpbi 201 1  |-  F : A
--> B
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726   A.wral 2707    e. cmpt 4268   -->wf 5452
This theorem is referenced by:  harf  7530  r0weon  7896  dfac2a  8012  ackbij1lem10  8111  cff  8130  isf32lem9  8243  fin1a2lem2  8283  fin1a2lem4  8285  ccatfn  11743  cjf  11911  ref  11919  imf  11920  absf  12143  limsupcl  12269  limsupgf  12271  eff  12686  sinf  12727  cosf  12728  bitsf  12941  fnum  13136  fden  13137  setcepi  14245  catcfuccl  14266  staffval  15937  ocvfval  16895  pjfval  16935  pjpm  16937  leordtval2  17278  lecldbas  17285  nmfval  18638  nmoffn  18747  nmofval  18750  divcn  18900  xrhmeo  18973  tchex  19178  tchnmfval  19188  ioorf  19467  dveflem  19865  resinf1o  20440  efifo  20451  logcnlem5  20539  resqrcn  20635  asinf  20714  acosf  20716  atanf  20722  leibpilem2  20783  areaf  20802  emcllem1  20836  chtf  20893  chpf  20908  ppif  20915  muf  20925  bposlem7  21076  pntrf  21259  pntrsumo1  21261  pntsf  21269  pntrlog2bndlem4  21276  pntrlog2bndlem5  21277  normf  22627  hosubcli  23274  cnlnadjlem4  23575  cnlnadjlem6  23577  igamf  24837  derangf  24856  snmlff  25018  sinccvglem  25111  circum  25113  cncfres  26476  lhe4.4ex1a  27525  clim1fr1  27705  wallispilem5  27796  wallispi  27797  stirlinglem5  27805  stirlinglem13  27813  stirlinglem14  27814  stirlinglem15  27815  stirlingr  27817  lsatset  29790
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pr 4405
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-mpt 4270  df-id 4500  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-fv 5464
  Copyright terms: Public domain W3C validator