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

Theorem fnmpti 5374
Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
fnmpti.1  |-  B  e. 
_V
fnmpti.2  |-  F  =  ( x  e.  A  |->  B )
Assertion
Ref Expression
fnmpti  |-  F  Fn  A
Distinct variable group:    x, A
Allowed substitution hints:    B( x)    F( x)

Proof of Theorem fnmpti
StepHypRef Expression
1 fnmpti.1 . . 3  |-  B  e. 
_V
21rgenw 2612 . 2  |-  A. x  e.  A  B  e.  _V
3 fnmpti.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43mptfng 5371 . 2  |-  ( A. x  e.  A  B  e.  _V  <->  F  Fn  A
)
52, 4mpbi 199 1  |-  F  Fn  A
Colors of variables: wff set class
Syntax hints:    = wceq 1625    e. wcel 1686   A.wral 2545   _Vcvv 2790    e. cmpt 4079    Fn wfn 5252
This theorem is referenced by:  dmmpti  5375  fconst  5429  dffn5  5570  eufnfv  5754  idref  5761  offn  6091  caofinvl  6106  fo1st  6141  fo2nd  6142  reldm  6173  mapsnf1o2  6817  unfilem2  7124  fidomdm  7140  pwfilem  7152  noinfep  7362  aceq3lem  7749  dfac4  7751  ackbij2lem2  7868  cfslb2n  7896  axcc2lem  8064  konigthlem  8192  rankcf  8401  tskuni  8407  seqf1o  11089  ccatlen  11432  swrdlen  11458  sqrf  11849  fsumrev  12243  fsumshft  12244  efcvgfsum  12369  prmreclem2  12966  1arith  12976  vdwlem6  13035  vdwlem8  13037  slotfn  13164  topnfn  13332  fnmre  13495  cidffn  13582  cidfn  13583  funcres  13772  yonedainv  14057  fn0g  14387  grpinvfn  14524  conjnmz  14718  odf  14854  sylow1lem4  14914  pgpssslw  14927  sylow2blem3  14935  sylow3lem2  14941  cygctb  15180  dprd2da  15279  fnmgp  15329  rlmfn  15946  asclfn  16078  fncld  16761  hauseqlcld  17342  kqf  17440  filunirn  17579  fmf  17642  txflf  17703  clsnsg  17794  tgpconcomp  17797  divstgpopn  17804  divstgplem  17805  xmetunirn  17904  met1stc  18069  ovolf  18843  vitali  18970  i1fmulc  19060  mbfi1fseqlem4  19075  itg2seq  19099  itg2monolem1  19107  i1fibl  19164  fncpn  19284  lhop1lem  19362  evlslem1  19401  mdegxrf  19456  aannenlem3  19712  logccv  20012  padicabvf  20782  fngid  20883  grpoinvf  20909  ipasslem8  21417  occllem  21884  pjfni  22282  pjmfn  22296  rnbra  22689  bra11  22690  kbass2  22699  hmopidmchi  22733  ballotlem7  23096  xppreima2  23214  abfmpunirn  23218  dmct  23344  dya2iocrfn  23582  mptelee  24525  itg2addnclem2  24934  itg2addnc  24935  npincppr  25170  sdclem2  26463  prdsbnd2  26530  rrncmslem  26567  rmxypairf1o  27007  frlmup4  27264  hbtlem6  27344  dgraaf  27363  psgnfn  27435  cytpfn  27538  addrfn  27688  subrfn  27689  mulvfn  27690  diafn  31297  cdlemm10N  31381  dibfna  31417  lcfrlem9  31813  mapd1o  31911  hdmapfnN  32095  hgmapfnN  32154
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-fun 5259  df-fn 5260
  Copyright terms: Public domain W3C validator