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

Theorem nfmpt 4124
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 4095 . 2  |-  ( y  e.  A  |->  B )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  B ) }
2 nfmpt.1 . . . . 5  |-  F/_ x A
32nfcri 2426 . . . 4  |-  F/ x  y  e.  A
4 nfmpt.2 . . . . 5  |-  F/_ x B
54nfeq2 2443 . . . 4  |-  F/ x  z  =  B
63, 5nfan 1783 . . 3  |-  F/ x
( y  e.  A  /\  z  =  B
)
76nfopab 4100 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  =  B ) }
81, 7nfcxfr 2429 1  |-  F/_ x
( y  e.  A  |->  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1632    e. wcel 1696   F/_wnfc 2419   {copab 4092    e. cmpt 4093
This theorem is referenced by:  nfof  6099  nfrdg  6443  mapxpen  7043  nfoi  7245  nfsum1  12179  nfsum  12180  fsumrlim  12285  fsumo1  12286  gsum2d2  15241  prdsgsum  15245  dprd2d2  15295  gsumdixp  15408  ptbasfi  17292  ptcnplem  17331  ptcnp  17332  cnmptk2  17396  cnmpt2k  17398  xkocnv  17521  fsumcn  18390  itg2cnlem1  19132  nfitg  19145  itgfsum  19197  dvmptfsum  19338  mpfrcl  19418  itgulm2  19801  fmptcof2  23244  nfcprod1  24132  nfcprod  24133  nfprod  25414  aomclem8  27262  refsum2cn  27812  fmuldfeq  27816  stoweidlem26  27878  stoweidlem31  27883  stoweidlem34  27886  stoweidlem35  27887  stoweidlem42  27894  stoweidlem48  27900  stoweidlem59  27911  bnj1366  29178  cdleme32d  31255  cdleme32f  31257  cdlemksv2  31658  cdlemkuv2  31678  hlhilset  32749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-opab 4094  df-mpt 4095
  Copyright terms: Public domain W3C validator