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

Theorem fnmpti 5515
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 2718 . 2  |-  A. x  e.  A  B  e.  _V
3 fnmpti.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43mptfng 5512 . 2  |-  ( A. x  e.  A  B  e.  _V  <->  F  Fn  A
)
52, 4mpbi 200 1  |-  F  Fn  A
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1717   A.wral 2651   _Vcvv 2901    e. cmpt 4209    Fn wfn 5391
This theorem is referenced by:  dmmpti  5516  fconst  5571  dffn5  5713  eufnfv  5913  idref  5920  offn  6257  caofinvl  6272  fo1st  6307  fo2nd  6308  reldm  6339  mapsnf1o2  6999  unfilem2  7310  fidomdm  7326  pwfilem  7338  noinfep  7549  aceq3lem  7936  dfac4  7938  ackbij2lem2  8055  cfslb2n  8083  axcc2lem  8251  konigthlem  8378  rankcf  8587  tskuni  8593  seqf1o  11293  ccatlen  11673  swrdlen  11699  sqrf  12096  fsumrev  12491  fsumshft  12492  efcvgfsum  12617  prmreclem2  13214  1arith  13224  vdwlem6  13283  vdwlem8  13285  slotfn  13412  topnfn  13582  fnmre  13745  cidffn  13832  cidfn  13833  funcres  14022  yonedainv  14307  fn0g  14637  grpinvfn  14774  conjnmz  14968  odf  15104  sylow1lem4  15164  pgpssslw  15177  sylow2blem3  15185  sylow3lem2  15191  cygctb  15430  dprd2da  15529  fnmgp  15579  rlmfn  16192  asclfn  16324  fncld  17011  hauseqlcld  17601  kqf  17702  filunirn  17837  fmf  17900  txflf  17961  clsnsg  18062  tgpconcomp  18065  divstgpopn  18072  divstgplem  18073  ustfn  18154  xmetunirn  18278  met1stc  18443  ovolf  19247  vitali  19374  i1fmulc  19464  mbfi1fseqlem4  19479  itg2seq  19503  itg2monolem1  19511  i1fibl  19568  fncpn  19688  lhop1lem  19766  evlslem1  19805  mdegxrf  19860  aannenlem3  20116  logccv  20423  padicabvf  21194  fngid  21652  grpoinvf  21678  occllem  22655  pjfni  23053  pjmfn  23067  rnbra  23460  bra11  23461  kbass2  23470  hmopidmchi  23504  xppreima2  23904  abfmpunirn  23908  dmct  23949  ofcfn  24281  sxbrsigalem3  24418  fprodshft  25081  fprodrev  25082  faclimlem1  25122  mptelee  25550  volsupnfl  25958  itg2addnclem2  25960  itg2addnc  25961  itgaddnclem2  25966  sdclem2  26139  prdsbnd2  26197  rrncmslem  26234  rmxypairf1o  26667  frlmup4  26924  hbtlem6  27004  dgraaf  27023  psgnfn  27095  cytpfn  27198  addrfn  27347  subrfn  27348  mulvfn  27349  diafn  31151  cdlemm10N  31235  dibfna  31271  lcfrlem9  31667  mapd1o  31765  hdmapfnN  31949  hgmapfnN  32008
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pr 4346
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-br 4156  df-opab 4210  df-mpt 4211  df-id 4441  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-fun 5398  df-fn 5399
  Copyright terms: Public domain W3C validator