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

Theorem nfmpt1 4111
Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
Assertion
Ref Expression
nfmpt1  |-  F/_ x
( x  e.  A  |->  B )
Dummy variable  z is distinct from all other variables.

Proof of Theorem nfmpt1
StepHypRef Expression
1 df-mpt 4081 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }
2 nfopab1 4087 . 2  |-  F/_ x { <. x ,  z
>.  |  ( x  e.  A  /\  z  =  B ) }
31, 2nfcxfr 2418 1  |-  F/_ x
( x  e.  A  |->  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 360    = wceq 1624    e. wcel 1685   F/_wnfc 2408   {copab 4078    e. cmpt 4079
This theorem is referenced by:  nffvmpt1  5494  fvmptss  5571  fvmptdf  5573  mpteqb  5576  fvmptt  5577  fvmptf  5578  ralrnmpt  5631  f1ompt  5644  fmptco  5653  f1mpt  5747  fliftfun  5773  offval2  6057  ofrfval2  6058  rdgsucmptf  6437  rdgsucmptnf  6438  frsucmpt  6446  frsucmptn  6447  mptelixpg  6849  dom2lem  6897  mapxpen  7023  cnfcom3clem  7404  infxpenc2lem2  7643  dfac8clem  7655  acni2  7669  acnlem  7671  fin23lem32  7966  axcc2  8059  axcc3  8060  ac6num  8102  axdclem  8142  rlim2  11965  ello1mpt  11990  o1compt  12056  nfsum1  12158  sumfc  12177  zsum  12186  fsum  12188  fsumf1o  12191  sumss  12192  fsumcvg2  12195  fsumadd  12206  isummulc2  12220  fsummulc2  12241  fsumrelem  12260  isumshft  12293  iserodd  12883  prdsbas3  13375  prdsdsval2  13378  yonedalem4b  14045  prdsgsum  15224  dprdwd  15241  gsumdixp  15387  evlslem4  16240  2ndcdisj  17177  elptr2  17264  ptunimpt  17285  ptcldmpt  17303  ptclsg  17304  txcnp  17309  ptcnplem  17310  ptcnp  17311  cnmpt11  17352  cnmpt1t  17354  cnmptk2  17375  xkocnv  17500  flfcnp2  17697  voliun  18906  mbfeqalem  18992  mbfpos  19001  mbfposr  19002  mbfposb  19003  mbfsup  19014  mbfinf  19015  mbflim  19018  i1fposd  19057  itg1climres  19064  itg2splitlem  19098  itg2split  19099  itg2cnlem1  19111  isibl2  19116  nfitg1  19123  itgmpt  19132  itgeqa  19163  itggt0  19191  itgcn  19192  dvlipcn  19336  lhop2  19357  dvfsumabs  19365  itgparts  19389  itgsubstlem  19390  itgsubst  19391  elplyd  19579  coeeq2  19619  dgrle  19620  ulmss  19769  itgulm2  19780  leibpi  20233  rlimcnp  20255  o1cxp  20264  lgseisenlem2  20584  cnlnadjlem5  22644  ballotlem7  23088  cvmcov  23199  trpredlem1  23632  trpredrec  23643  prodeq3ii  24708  nfprod1  24710  prodeqfv  24718  fprodadd  24752  fprodneg  24778  fprodsub  24779  trooo  24794  trinv  24795  ltrinvlem  24806  rltrooo  24815  svli2  24884  cnegvex2  25060  rnegvex2  25061  totbndbnd  25913  elrfirn2  26171  mzpsubmpt  26221  eq0rabdioph  26256  eqrabdioph  26257  monotoddzz  26428  aomclem8  26559  refsumcn  27101  refsum2cnlem1  27108  fmuldfeqlem1  27112  fmuldfeq  27113  climneg  27136  climdivf  27138  itgsin0pilem1  27144  ibliccsinexp  27145  itgsinexplem1  27148  itgsinexp  27149  stoweidlem16  27165  stoweidlem18  27167  stoweidlem19  27168  stoweidlem20  27169  stoweidlem22  27171  stoweidlem23  27172  stoweidlem27  27176  stoweidlem31  27180  stoweidlem32  27181  stoweidlem34  27183  stoweidlem35  27184  stoweidlem36  27185  stoweidlem40  27189  stoweidlem41  27190  stoweidlem42  27191  stoweidlem43  27192  stoweidlem44  27193  stoweidlem45  27194  stoweidlem48  27197  stoweidlem51  27200  stoweidlem55  27204  stoweidlem59  27208  stoweidlem60  27209  stoweidlem62  27211  wallispilem5  27218  stirlinglem4  27226  stirlinglem5  27227  stirlinglem8  27230  stirlinglem11  27233  stirlinglem12  27234  stirlinglem13  27235  stirlinglem14  27236  stirlinglem15  27237  stirling  27238
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-opab 4080  df-mpt 4081
  Copyright terms: Public domain W3C validator