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

Theorem fnmpti 5372
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 2610 . 2  |-  A. x  e.  A  B  e.  _V
3 fnmpti.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43mptfng 5369 . 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 1623    e. wcel 1684   A.wral 2543   _Vcvv 2788    e. cmpt 4077    Fn wfn 5250
This theorem is referenced by:  dmmpti  5373  fconst  5427  dffn5  5568  eufnfv  5752  idref  5759  offn  6089  caofinvl  6104  fo1st  6139  fo2nd  6140  reldm  6171  mapsnf1o2  6815  unfilem2  7122  fidomdm  7138  pwfilem  7150  noinfep  7360  aceq3lem  7747  dfac4  7749  ackbij2lem2  7866  cfslb2n  7894  axcc2lem  8062  konigthlem  8190  rankcf  8399  tskuni  8405  seqf1o  11087  ccatlen  11430  swrdlen  11456  sqrf  11847  fsumrev  12241  fsumshft  12242  efcvgfsum  12367  prmreclem2  12964  1arith  12974  vdwlem6  13033  vdwlem8  13035  slotfn  13162  topnfn  13330  fnmre  13493  cidffn  13580  cidfn  13581  funcres  13770  yonedainv  14055  fn0g  14385  grpinvfn  14522  conjnmz  14716  odf  14852  sylow1lem4  14912  pgpssslw  14925  sylow2blem3  14933  sylow3lem2  14939  cygctb  15178  dprd2da  15277  fnmgp  15327  rlmfn  15944  asclfn  16076  fncld  16759  hauseqlcld  17340  kqf  17438  filunirn  17577  fmf  17640  txflf  17701  clsnsg  17792  tgpconcomp  17795  divstgpopn  17802  divstgplem  17803  xmetunirn  17902  met1stc  18067  ovolf  18841  vitali  18968  i1fmulc  19058  mbfi1fseqlem4  19073  itg2seq  19097  itg2monolem1  19105  i1fibl  19162  fncpn  19282  lhop1lem  19360  evlslem1  19399  mdegxrf  19454  aannenlem3  19710  logccv  20010  padicabvf  20780  fngid  20881  grpoinvf  20907  ipasslem8  21415  occllem  21882  pjfni  22280  pjmfn  22294  rnbra  22687  bra11  22688  kbass2  22697  hmopidmchi  22731  ballotlem7  23094  xppreima2  23212  abfmpunirn  23216  dmct  23342  dya2iocrfn  23580  mptelee  24523  npincppr  25159  sdclem2  26452  prdsbnd2  26519  rrncmslem  26556  rmxypairf1o  26996  frlmup4  27253  hbtlem6  27333  dgraaf  27352  psgnfn  27424  cytpfn  27527  addrfn  27677  subrfn  27678  mulvfn  27679  diafn  31224  cdlemm10N  31308  dibfna  31344  lcfrlem9  31740  mapd1o  31838  hdmapfnN  32022  hgmapfnN  32081
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-fun 5257  df-fn 5258
  Copyright terms: Public domain W3C validator