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

Theorem fnmpti 5536
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 2737 . 2  |-  A. x  e.  A  B  e.  _V
3 fnmpti.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
43mptfng 5533 . 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 1721   A.wral 2670   _Vcvv 2920    e. cmpt 4230    Fn wfn 5412
This theorem is referenced by:  dmmpti  5537  fconst  5592  dffn5  5735  eufnfv  5935  idref  5942  offn  6279  caofinvl  6294  fo1st  6329  fo2nd  6330  reldm  6361  mapsnf1o2  7024  unfilem2  7335  fidomdm  7351  pwfilem  7363  noinfep  7574  aceq3lem  7961  dfac4  7963  ackbij2lem2  8080  cfslb2n  8108  axcc2lem  8276  konigthlem  8403  rankcf  8612  tskuni  8618  seqf1o  11323  ccatlen  11703  swrdlen  11729  sqrf  12126  fsumrev  12521  fsumshft  12522  efcvgfsum  12647  prmreclem2  13244  1arith  13254  vdwlem6  13313  vdwlem8  13315  slotfn  13442  topnfn  13612  fnmre  13775  cidffn  13862  cidfn  13863  funcres  14052  yonedainv  14337  fn0g  14667  grpinvfn  14804  conjnmz  14998  odf  15134  sylow1lem4  15194  pgpssslw  15207  sylow2blem3  15215  sylow3lem2  15221  cygctb  15460  dprd2da  15559  fnmgp  15609  rlmfn  16222  asclfn  16354  fncld  17045  hauseqlcld  17635  kqf  17736  filunirn  17871  fmf  17934  txflf  17995  clsnsg  18096  tgpconcomp  18099  divstgpopn  18106  divstgplem  18107  ustfn  18188  xmetunirn  18324  met1stc  18508  ovolf  19335  vitali  19462  i1fmulc  19552  mbfi1fseqlem4  19567  itg2seq  19591  itg2monolem1  19599  i1fibl  19656  fncpn  19776  lhop1lem  19854  evlslem1  19893  mdegxrf  19948  aannenlem3  20204  logccv  20511  padicabvf  21282  fngid  21759  grpoinvf  21785  occllem  22762  pjfni  23160  pjmfn  23174  rnbra  23567  bra11  23568  kbass2  23577  hmopidmchi  23611  xppreima2  24017  abfmpunirn  24021  dmct  24063  ofcfn  24440  sxbrsigalem3  24579  fprodshft  25257  fprodrev  25258  faclimlem1  25314  mptelee  25742  mblfinlem  26147  volsupnfl  26154  cnambfre  26158  itg2addnclem2  26160  itg2addnclem3  26161  sdclem2  26340  prdsbnd2  26398  rrncmslem  26435  rmxypairf1o  26868  frlmup4  27125  hbtlem6  27205  dgraaf  27224  psgnfn  27296  cytpfn  27399  addrfn  27548  subrfn  27549  mulvfn  27550  swrdvalfn  28011  ccatvalfn  28012  swrdswrd  28015  diafn  31521  cdlemm10N  31605  dibfna  31641  lcfrlem9  32037  mapd1o  32135  hdmapfnN  32319  hgmapfnN  32378
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 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367
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 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-fun 5419  df-fn 5420
  Copyright terms: Public domain W3C validator