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

Theorem nfmpt 4108
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 4079 . 2  |-  ( y  e.  A  |->  B )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  B ) }
2 nfmpt.1 . . . . 5  |-  F/_ x A
32nfcri 2413 . . . 4  |-  F/ x  y  e.  A
4 nfmpt.2 . . . . 5  |-  F/_ x B
54nfeq2 2430 . . . 4  |-  F/ x  z  =  B
63, 5nfan 1771 . . 3  |-  F/ x
( y  e.  A  /\  z  =  B
)
76nfopab 4084 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  =  B ) }
81, 7nfcxfr 2416 1  |-  F/_ x
( y  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:  nfof  6083  nfrdg  6427  mapxpen  7027  nfoi  7229  nfsum1  12163  nfsum  12164  fsumrlim  12269  fsumo1  12270  gsum2d2  15225  prdsgsum  15229  dprd2d2  15279  gsumdixp  15392  ptbasfi  17276  ptcnplem  17315  ptcnp  17316  cnmptk2  17380  cnmpt2k  17382  xkocnv  17505  fsumcn  18374  itg2cnlem1  19116  nfitg  19129  itgfsum  19181  dvmptfsum  19322  mpfrcl  19402  itgulm2  19785  fmptcof2  23229  nfprod  25311  aomclem8  27159  refsum2cn  27709  fmuldfeq  27713  stoweidlem26  27775  stoweidlem31  27780  stoweidlem34  27783  stoweidlem35  27784  stoweidlem42  27791  stoweidlem48  27797  stoweidlem59  27808  bnj1366  28862  cdleme32d  30633  cdleme32f  30635  cdlemksv2  31036  cdlemkuv2  31056  hlhilset  32127
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-or 359  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