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

Theorem nfmpt 4289
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 4260 . 2  |-  ( y  e.  A  |->  B )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  B ) }
2 nfmpt.1 . . . . 5  |-  F/_ x A
32nfcri 2565 . . . 4  |-  F/ x  y  e.  A
4 nfmpt.2 . . . . 5  |-  F/_ x B
54nfeq2 2582 . . . 4  |-  F/ x  z  =  B
63, 5nfan 1846 . . 3  |-  F/ x
( y  e.  A  /\  z  =  B
)
76nfopab 4265 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  =  B ) }
81, 7nfcxfr 2568 1  |-  F/_ x
( y  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:  nfrdg  6664  mapxpen  7265  nfoi  7475  seqof2  11373  nfsum1  12476  nfsum  12477  fsumrlim  12582  fsumo1  12583  gsum2d2  15540  prdsgsum  15544  dprd2d2  15594  gsumdixp  15707  ptbasfi  17605  ptcnplem  17645  ptcnp  17646  cnmptk2  17710  cnmpt2k  17712  xkocnv  17838  fsumcn  18892  itg2cnlem1  19645  nfitg  19658  itgfsum  19710  dvmptfsum  19851  mpfrcl  19931  itgulm2  20317  fmptcof2  24068  lgamgulm2  24812  nfcprod1  25228  nfcprod  25229  aomclem8  27127  refsum2cn  27676  fmuldfeq  27680  stoweidlem26  27742  stoweidlem31  27747  stoweidlem34  27750  stoweidlem35  27751  stoweidlem42  27758  stoweidlem48  27764  stoweidlem59  27775  bnj1366  29138  cdleme32d  31178  cdleme32f  31180  cdlemksv2  31581  cdlemkuv2  31601  hlhilset  32672
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-or 360  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