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

Theorem nfmpt1 4188
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 )

Proof of Theorem nfmpt1
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 df-mpt 4158 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }
2 nfopab1 4164 . 2  |-  F/_ x { <. x ,  z
>.  |  ( x  e.  A  /\  z  =  B ) }
31, 2nfcxfr 2491 1  |-  F/_ x
( x  e.  A  |->  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1642    e. wcel 1710   F/_wnfc 2481   {copab 4155    e. cmpt 4156
This theorem is referenced by:  nffvmpt1  5613  fvmptss  5689  fvmptdf  5691  mpteqb  5694  fvmptt  5695  fvmptf  5696  ralrnmpt  5749  f1ompt  5762  fmptco  5771  f1mpt  5869  fliftfun  5895  offval2  6179  ofrfval2  6180  rdgsucmptf  6525  rdgsucmptnf  6526  frsucmpt  6534  frsucmptn  6535  mptelixpg  6938  dom2lem  6986  mapxpen  7112  cnfcom3clem  7495  infxpenc2lem2  7734  dfac8clem  7746  acni2  7760  acnlem  7762  fin23lem32  8057  axcc2  8150  axcc3  8151  ac6num  8193  axdclem  8233  rlim2  12060  ello1mpt  12085  o1compt  12151  nfsum1  12254  sumfc  12273  zsum  12282  fsum  12284  fsumf1o  12287  sumss  12288  fsumcvg2  12291  fsumadd  12302  isummulc2  12316  fsummulc2  12337  fsumrelem  12356  isumshft  12389  iserodd  12979  prdsbas3  13473  prdsdsval2  13476  yonedalem4b  14143  prdsgsum  15322  dprdwd  15339  gsumdixp  15485  evlslem4  16338  2ndcdisj  17282  elptr2  17369  ptunimpt  17390  ptcldmpt  17408  ptclsg  17409  txcnp  17414  ptcnplem  17415  ptcnp  17416  cnmpt11  17457  cnmpt1t  17459  cnmptk2  17480  xkocnv  17605  flfcnp2  17798  voliun  19009  mbfeqalem  19095  mbfpos  19104  mbfposr  19105  mbfposb  19106  mbfsup  19117  mbfinf  19118  mbflim  19121  i1fposd  19160  itg1climres  19167  itg2splitlem  19201  itg2split  19202  itg2cnlem1  19214  isibl2  19219  nfitg1  19226  itgmpt  19235  itgeqa  19266  itggt0  19294  itgcn  19295  dvlipcn  19439  lhop2  19460  dvfsumabs  19468  itgparts  19492  itgsubstlem  19493  itgsubst  19494  elplyd  19682  coeeq2  19722  dgrle  19723  ulmss  19874  itgulm2  19886  leibpi  20343  rlimcnp  20365  o1cxp  20374  lgseisenlem2  20695  cnlnadjlem5  22759  fmptcof2  23277  offval2f  23281  disjdsct  23291  neiptopreu  23446  utopsnneiplem  23551  restmetu  23615  nfesum1  23703  esumc  23712  voliune  23849  rrvadd  23959  ballotlem7  24042  lgamgulm2  24069  cvmcov  24198  nfcprod1  24537  zprod  24564  prodfc  24572  fprodf1o  24573  trpredlem1  24788  trpredrec  24799  totbndbnd  25836  elrfirn2  26094  mzpsubmpt  26144  eq0rabdioph  26179  eqrabdioph  26180  monotoddzz  26351  aomclem8  26482  refsumcn  27024  refsum2cnlem1  27031  fmuldfeqlem1  27035  fmuldfeq  27036  climneg  27059  climdivf  27061  itgsin0pilem1  27067  ibliccsinexp  27068  itgsinexplem1  27071  itgsinexp  27072  stoweidlem16  27088  stoweidlem18  27090  stoweidlem19  27091  stoweidlem20  27092  stoweidlem22  27094  stoweidlem23  27095  stoweidlem27  27099  stoweidlem31  27103  stoweidlem32  27104  stoweidlem34  27106  stoweidlem35  27107  stoweidlem36  27108  stoweidlem40  27112  stoweidlem41  27113  stoweidlem42  27114  stoweidlem43  27115  stoweidlem44  27116  stoweidlem45  27117  stoweidlem48  27120  stoweidlem51  27123  stoweidlem55  27127  stoweidlem59  27131  stoweidlem60  27132  stoweidlem62  27134  wallispilem5  27141  stirlinglem4  27149  stirlinglem5  27150  stirlinglem8  27153  stirlinglem11  27156  stirlinglem12  27157  stirlinglem13  27158  stirlinglem14  27159  stirlinglem15  27160  stirling  27161
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-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-opab 4157  df-mpt 4158
  Copyright terms: Public domain W3C validator