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

Theorem fnmpti 5454
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 2686 . 2  |-  A. x  e.  A  B  e.  _V
3 fnmpti.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43mptfng 5451 . 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 1642    e. wcel 1710   A.wral 2619   _Vcvv 2864    e. cmpt 4158    Fn wfn 5332
This theorem is referenced by:  dmmpti  5455  fconst  5510  dffn5  5651  eufnfv  5838  idref  5845  offn  6176  caofinvl  6191  fo1st  6226  fo2nd  6227  reldm  6258  mapsnf1o2  6903  unfilem2  7212  fidomdm  7228  pwfilem  7240  noinfep  7450  aceq3lem  7837  dfac4  7839  ackbij2lem2  7956  cfslb2n  7984  axcc2lem  8152  konigthlem  8280  rankcf  8489  tskuni  8495  seqf1o  11179  ccatlen  11526  swrdlen  11552  sqrf  11943  fsumrev  12338  fsumshft  12339  efcvgfsum  12464  prmreclem2  13061  1arith  13071  vdwlem6  13130  vdwlem8  13132  slotfn  13259  topnfn  13429  fnmre  13592  cidffn  13679  cidfn  13680  funcres  13869  yonedainv  14154  fn0g  14484  grpinvfn  14621  conjnmz  14815  odf  14951  sylow1lem4  15011  pgpssslw  15024  sylow2blem3  15032  sylow3lem2  15038  cygctb  15277  dprd2da  15376  fnmgp  15426  rlmfn  16043  asclfn  16175  fncld  16865  hauseqlcld  17446  kqf  17544  filunirn  17679  fmf  17742  txflf  17803  clsnsg  17894  tgpconcomp  17897  divstgpopn  17904  divstgplem  17905  xmetunirn  18004  met1stc  18169  ovolf  18945  vitali  19072  i1fmulc  19162  mbfi1fseqlem4  19177  itg2seq  19201  itg2monolem1  19209  i1fibl  19266  fncpn  19386  lhop1lem  19464  evlslem1  19503  mdegxrf  19558  aannenlem3  19814  logccv  20121  padicabvf  20892  fngid  20993  grpoinvf  21019  ipasslem8  21529  occllem  21996  pjfni  22394  pjmfn  22408  rnbra  22801  bra11  22802  kbass2  22811  hmopidmchi  22845  xppreima2  23263  abfmpunirn  23267  dmct  23310  ustfn  23507  ballotlem7  24042  fprodshft  24601  fprodrev  24602  fngamma  24644  faclimlem1  24654  mptelee  25082  volsupnfl  25491  itg2addnclem2  25493  itg2addnc  25494  itgaddnclem2  25499  sdclem2  25776  prdsbnd2  25842  rrncmslem  25879  rmxypairf1o  26319  frlmup4  26576  hbtlem6  26656  dgraaf  26675  psgnfn  26747  cytpfn  26850  addrfn  27000  subrfn  27001  mulvfn  27002  diafn  31293  cdlemm10N  31377  dibfna  31413  lcfrlem9  31809  mapd1o  31907  hdmapfnN  32091  hgmapfnN  32150
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pr 4295
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-fun 5339  df-fn 5340
  Copyright terms: Public domain W3C validator