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

Theorem nfmpt 4238
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 4209 . 2  |-  ( y  e.  A  |->  B )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  B ) }
2 nfmpt.1 . . . . 5  |-  F/_ x A
32nfcri 2517 . . . 4  |-  F/ x  y  e.  A
4 nfmpt.2 . . . . 5  |-  F/_ x B
54nfeq2 2534 . . . 4  |-  F/ x  z  =  B
63, 5nfan 1836 . . 3  |-  F/ x
( y  e.  A  /\  z  =  B
)
76nfopab 4214 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  =  B ) }
81, 7nfcxfr 2520 1  |-  F/_ x
( y  e.  A  |->  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 359    = wceq 1649    e. wcel 1717   F/_wnfc 2510   {copab 4206    e. cmpt 4207
This theorem is referenced by:  nfrdg  6608  mapxpen  7209  nfoi  7416  seqof2  11308  nfsum1  12411  nfsum  12412  fsumrlim  12517  fsumo1  12518  gsum2d2  15475  prdsgsum  15479  dprd2d2  15529  gsumdixp  15642  ptbasfi  17534  ptcnplem  17574  ptcnp  17575  cnmptk2  17639  cnmpt2k  17641  xkocnv  17767  fsumcn  18771  itg2cnlem1  19520  nfitg  19533  itgfsum  19585  dvmptfsum  19726  mpfrcl  19806  itgulm2  20192  fmptcof2  23918  lgamgulm2  24599  nfcprod1  25015  nfcprod  25016  aomclem8  26828  refsum2cn  27377  fmuldfeq  27381  stoweidlem26  27443  stoweidlem31  27448  stoweidlem34  27451  stoweidlem35  27452  stoweidlem42  27459  stoweidlem48  27465  stoweidlem59  27476  bnj1366  28539  cdleme32d  30558  cdleme32f  30560  cdlemksv2  30961  cdlemkuv2  30981  hlhilset  32052
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-opab 4208  df-mpt 4209
  Copyright terms: Public domain W3C validator