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

Theorem nfmpt 4535
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 4507 . 2  |-  ( y  e.  A  |->  B )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  B ) }
2 nfmpt.1 . . . . 5  |-  F/_ x A
32nfcri 2622 . . . 4  |-  F/ x  y  e.  A
4 nfmpt.2 . . . . 5  |-  F/_ x B
54nfeq2 2646 . . . 4  |-  F/ x  z  =  B
63, 5nfan 1875 . . 3  |-  F/ x
( y  e.  A  /\  z  =  B
)
76nfopab 4512 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  =  B ) }
81, 7nfcxfr 2627 1  |-  F/_ x
( y  e.  A  |->  B )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1379    e. wcel 1767   F/_wnfc 2615   {copab 4504    |-> cmpt 4505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-opab 4506  df-mpt 4507
This theorem is referenced by:  ovmpt3rab1  6516  mpt2curryvald  6996  nfrdg  7077  mapxpen  7680  nfoi  7935  seqof2  12128  nfsum1  13468  nfsum  13469  fsumrlim  13581  fsumo1  13582  gsum2d2  16790  prdsgsum  16795  prdsgsumOLD  16796  dprd2d2  16880  gsumdixpOLD  17038  gsumdixp  17039  mpfrcl  17955  ptbasfi  19814  ptcnplem  19854  ptcnp  19855  cnmptk2  19919  cnmpt2k  19921  xkocnv  20047  fsumcn  21106  itg2cnlem1  21900  nfitg  21913  itgfsum  21965  dvmptfsum  22108  itgulm2  22535  fmptcof2  27171  fpwrelmap  27225  oms0  27903  lgamgulm2  28215  nfcprod1  28616  nfcprod  28617  aomclem8  30611  refsum2cn  30991  fmuldfeq  31133  stoweidlem26  31326  stoweidlem31  31331  stoweidlem34  31334  stoweidlem35  31335  stoweidlem42  31342  stoweidlem48  31348  stoweidlem59  31359  fourierdlem31  31438  fourierdlem112  31519  bnj1366  32967  cdleme32d  35240  cdleme32f  35242  cdlemksv2  35643  cdlemkuv2  35663  hlhilset  36734
  Copyright terms: Public domain W3C validator