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

Theorem nfmpt1 4109
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 4079 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }
2 nfopab1 4085 . 2  |-  F/_ x { <. x ,  z
>.  |  ( x  e.  A  /\  z  =  B ) }
31, 2nfcxfr 2416 1  |-  F/_ x
( x  e.  A  |->  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1623    e. wcel 1684   F/_wnfc 2406   {copab 4076    e. cmpt 4077
This theorem is referenced by:  nffvmpt1  5533  fvmptss  5609  fvmptdf  5611  mpteqb  5614  fvmptt  5615  fvmptf  5616  ralrnmpt  5669  f1ompt  5682  fmptco  5691  f1mpt  5785  fliftfun  5811  offval2  6095  ofrfval2  6096  rdgsucmptf  6441  rdgsucmptnf  6442  frsucmpt  6450  frsucmptn  6451  mptelixpg  6853  dom2lem  6901  mapxpen  7027  cnfcom3clem  7408  infxpenc2lem2  7647  dfac8clem  7659  acni2  7673  acnlem  7675  fin23lem32  7970  axcc2  8063  axcc3  8064  ac6num  8106  axdclem  8146  rlim2  11970  ello1mpt  11995  o1compt  12061  nfsum1  12163  sumfc  12182  zsum  12191  fsum  12193  fsumf1o  12196  sumss  12197  fsumcvg2  12200  fsumadd  12211  isummulc2  12225  fsummulc2  12246  fsumrelem  12265  isumshft  12298  iserodd  12888  prdsbas3  13380  prdsdsval2  13383  yonedalem4b  14050  prdsgsum  15229  dprdwd  15246  gsumdixp  15392  evlslem4  16245  2ndcdisj  17182  elptr2  17269  ptunimpt  17290  ptcldmpt  17308  ptclsg  17309  txcnp  17314  ptcnplem  17315  ptcnp  17316  cnmpt11  17357  cnmpt1t  17359  cnmptk2  17380  xkocnv  17505  flfcnp2  17702  voliun  18911  mbfeqalem  18997  mbfpos  19006  mbfposr  19007  mbfposb  19008  mbfsup  19019  mbfinf  19020  mbflim  19023  i1fposd  19062  itg1climres  19069  itg2splitlem  19103  itg2split  19104  itg2cnlem1  19116  isibl2  19121  nfitg1  19128  itgmpt  19137  itgeqa  19168  itggt0  19196  itgcn  19197  dvlipcn  19341  lhop2  19362  dvfsumabs  19370  itgparts  19394  itgsubstlem  19395  itgsubst  19396  elplyd  19584  coeeq2  19624  dgrle  19625  ulmss  19774  itgulm2  19785  leibpi  20238  rlimcnp  20260  o1cxp  20269  lgseisenlem2  20589  cnlnadjlem5  22651  ballotlem7  23094  fmptcof2  23229  offval2f  23233  disjdsct  23369  esumc  23430  cvmcov  23794  trpredlem1  24230  trpredrec  24241  prodeq3ii  25308  nfprod1  25310  prodeqfv  25318  fprodadd  25352  fprodneg  25378  fprodsub  25379  trooo  25394  trinv  25395  ltrinvlem  25406  rltrooo  25415  svli2  25484  cnegvex2  25660  rnegvex2  25661  totbndbnd  26513  elrfirn2  26771  mzpsubmpt  26821  eq0rabdioph  26856  eqrabdioph  26857  monotoddzz  27028  aomclem8  27159  refsumcn  27701  refsum2cnlem1  27708  fmuldfeqlem1  27712  fmuldfeq  27713  climneg  27736  climdivf  27738  itgsin0pilem1  27744  ibliccsinexp  27745  itgsinexplem1  27748  itgsinexp  27749  stoweidlem16  27765  stoweidlem18  27767  stoweidlem19  27768  stoweidlem20  27769  stoweidlem22  27771  stoweidlem23  27772  stoweidlem27  27776  stoweidlem31  27780  stoweidlem32  27781  stoweidlem34  27783  stoweidlem35  27784  stoweidlem36  27785  stoweidlem40  27789  stoweidlem41  27790  stoweidlem42  27791  stoweidlem43  27792  stoweidlem44  27793  stoweidlem45  27794  stoweidlem48  27797  stoweidlem51  27800  stoweidlem55  27804  stoweidlem59  27808  stoweidlem60  27809  stoweidlem62  27811  wallispilem5  27818  stirlinglem4  27826  stirlinglem5  27827  stirlinglem8  27830  stirlinglem11  27833  stirlinglem12  27834  stirlinglem13  27835  stirlinglem14  27836  stirlinglem15  27837  stirling  27838
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-opab 4078  df-mpt 4079
  Copyright terms: Public domain W3C validator