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

Theorem nfmpt1 4290
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 4260 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }
2 nfopab1 4266 . 2  |-  F/_ x { <. x ,  z
>.  |  ( x  e.  A  /\  z  =  B ) }
31, 2nfcxfr 2568 1  |-  F/_ x
( x  e.  A  |->  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 359    = wceq 1652    e. wcel 1725   F/_wnfc 2558   {copab 4257    e. cmpt 4258
This theorem is referenced by:  nffvmpt1  5727  fvmptss  5804  fvmptdf  5807  mpteqb  5810  fvmptf  5812  ralrnmpt  5869  f1ompt  5882  f1mpt  5998  fliftfun  6025  rdgsucmptf  6677  rdgsucmptnf  6678  frsucmpt  6686  frsucmptn  6687  dom2lem  7138  mapxpen  7264  cnfcom3clem  7651  infxpenc2lem2  7890  dfac8clem  7902  acnlem  7918  fin23lem32  8213  axcc3  8307  ac6num  8348  nfsum1  12472  yonedalem4b  14361  prdsgsum  15540  neiptopreu  17185  2ndcdisj  17507  ptcnp  17642  cnmpt11  17683  cnmptk2  17706  xkocnv  17834  utopsnneiplem  18265  restmetu  18605  mbfposr  19532  mbfsup  19544  itg1climres  19594  itg2splitlem  19628  itg2split  19629  itg2cnlem1  19641  nfitg1  19653  dvlipcn  19866  lhop2  19887  dvfsumabs  19895  itgparts  19919  itgsubstlem  19920  itgulm2  20313  lgseisenlem2  21122  cnlnadjlem5  23562  ofpreima  24069  disjdsct  24078  nfesum1  24425  esumc  24434  voliune  24573  rrvadd  24698  ballotlem7  24781  lgamgulm2  24808  cvmcov  24938  nfcprod1  25225  trpredlem1  25485  trpredrec  25496  itg2addnclem  26202  totbndbnd  26435  mzpsubmpt  26737  eq0rabdioph  26772  eqrabdioph  26773  aomclem8  27074  refsumcn  27615  refsum2cnlem1  27622  fmuldfeqlem1  27626  fmuldfeq  27627  climneg  27650  climdivf  27652  itgsin0pilem1  27658  ibliccsinexp  27659  itgsinexplem1  27662  itgsinexp  27663  stoweidlem16  27679  stoweidlem18  27681  stoweidlem19  27682  stoweidlem20  27683  stoweidlem22  27685  stoweidlem23  27686  stoweidlem27  27690  stoweidlem31  27694  stoweidlem32  27695  stoweidlem34  27697  stoweidlem35  27698  stoweidlem36  27699  stoweidlem40  27703  stoweidlem41  27704  stoweidlem42  27705  stoweidlem43  27706  stoweidlem44  27707  stoweidlem45  27708  stoweidlem48  27711  stoweidlem51  27714  stoweidlem55  27718  stoweidlem59  27722  stoweidlem60  27723  stoweidlem62  27725  wallispilem5  27732  stirlinglem4  27740  stirlinglem5  27741  stirlinglem8  27744  stirlinglem11  27747  stirlinglem12  27748  stirlinglem13  27749  stirlinglem14  27750  stirlinglem15  27751  stirling  27752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-opab 4259  df-mpt 4260
  Copyright terms: Public domain W3C validator