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

Theorem nfmpt 4257
Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
Hypotheses
Ref Expression
nfmpt.1  |-  F/_ x A
nfmpt.2  |-  F/_ x B
Assertion
Ref Expression
nfmpt  |-  F/_ x
( y  e.  A  |->  B )
Distinct variable group:    x, y
Allowed substitution hints:    A( x, y)    B( x, y)

Proof of Theorem nfmpt
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 df-mpt 4228 . 2  |-  ( y  e.  A  |->  B )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  B ) }
2 nfmpt.1 . . . . 5  |-  F/_ x A
32nfcri 2534 . . . 4  |-  F/ x  y  e.  A
4 nfmpt.2 . . . . 5  |-  F/_ x B
54nfeq2 2551 . . . 4  |-  F/ x  z  =  B
63, 5nfan 1842 . . 3  |-  F/ x
( y  e.  A  /\  z  =  B
)
76nfopab 4233 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  =  B ) }
81, 7nfcxfr 2537 1  |-  F/_ x
( y  e.  A  |->  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 359    = wceq 1649    e. wcel 1721   F/_wnfc 2527   {copab 4225    e. cmpt 4226
This theorem is referenced by:  nfrdg  6631  mapxpen  7232  nfoi  7439  seqof2  11336  nfsum1  12439  nfsum  12440  fsumrlim  12545  fsumo1  12546  gsum2d2  15503  prdsgsum  15507  dprd2d2  15557  gsumdixp  15670  ptbasfi  17566  ptcnplem  17606  ptcnp  17607  cnmptk2  17671  cnmpt2k  17673  xkocnv  17799  fsumcn  18853  itg2cnlem1  19606  nfitg  19619  itgfsum  19671  dvmptfsum  19812  mpfrcl  19892  itgulm2  20278  fmptcof2  24029  lgamgulm2  24773  nfcprod1  25189  nfcprod  25190  aomclem8  27027  refsum2cn  27576  fmuldfeq  27580  stoweidlem26  27642  stoweidlem31  27647  stoweidlem34  27650  stoweidlem35  27651  stoweidlem42  27658  stoweidlem48  27664  stoweidlem59  27675  bnj1366  28907  cdleme32d  30926  cdleme32f  30928  cdlemksv2  31329  cdlemkuv2  31349  hlhilset  32420
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-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-opab 4227  df-mpt 4228
  Copyright terms: Public domain W3C validator