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

Theorem fmpti 5861
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 2776 . 2  |-  A. x  e.  A  C  e.  B
3 fmpt.1 . . 3  |-  F  =  ( x  e.  A  |->  C )
43fmpt 5859 . 2  |-  ( A. x  e.  A  C  e.  B  <->  F : A --> B )
52, 4mpbi 208 1  |-  F : A
--> B
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   A.wral 2710    e. cmpt 4345   -->wf 5409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421
This theorem is referenced by:  harf  7767  r0weon  8171  dfac2a  8291  ackbij1lem10  8390  cff  8409  isf32lem9  8522  fin1a2lem2  8562  fin1a2lem4  8564  ccatfn  12264  cjf  12585  ref  12593  imf  12594  absf  12817  limsupcl  12943  limsupgf  12945  eff  13359  sinf  13400  cosf  13401  bitsf  13615  fnum  13812  fden  13813  setcepi  14948  catcfuccl  14969  staffval  16910  ocvfval  18066  pjfval  18106  pjpm  18108  leordtval2  18791  lecldbas  18798  nmfval  20156  nmoffn  20265  nmofval  20268  divcn  20419  xrhmeo  20493  tchex  20707  tchnmfval  20718  ioorf  21028  dveflem  21426  resinf1o  21967  efifo  21978  logcnlem5  22066  resqrcn  22162  asinf  22242  acosf  22244  atanf  22250  leibpilem2  22311  areaf  22330  emcllem1  22364  chtf  22421  chpf  22436  ppif  22443  muf  22453  bposlem7  22604  pntrf  22787  pntrsumo1  22789  pntsf  22797  pntrlog2bndlem4  22804  pntrlog2bndlem5  22805  normf  24476  hosubcli  25124  cnlnadjlem4  25425  cnlnadjlem6  25427  eulerpartlemsf  26694  fiblem  26733  igamf  26989  derangf  27008  snmlff  27170  sinccvglem  27268  circum  27270  cncfres  28617  lhe4.4ex1a  29556  clim1fr1  29727  wallispilem5  29817  wallispi  29818  stirlinglem5  29826  stirlinglem13  29834  stirlinglem14  29835  stirlinglem15  29836  stirlingr  29838  lsatset  32475
  Copyright terms: Public domain W3C validator