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

Theorem nfmpt 4368
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 4340 . 2  |-  ( y  e.  A  |->  B )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  B ) }
2 nfmpt.1 . . . . 5  |-  F/_ x A
32nfcri 2563 . . . 4  |-  F/ x  y  e.  A
4 nfmpt.2 . . . . 5  |-  F/_ x B
54nfeq2 2580 . . . 4  |-  F/ x  z  =  B
63, 5nfan 1859 . . 3  |-  F/ x
( y  e.  A  /\  z  =  B
)
76nfopab 4345 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  =  B ) }
81, 7nfcxfr 2566 1  |-  F/_ x
( y  e.  A  |->  B )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1362    e. wcel 1755   F/_wnfc 2556   {copab 4337    e. cmpt 4338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-opab 4339  df-mpt 4340
This theorem is referenced by:  nfrdg  6856  mapxpen  7465  nfoi  7716  seqof2  11848  nfsum1  13151  nfsum  13152  fsumrlim  13257  fsumo1  13258  gsum2d2  16440  prdsgsum  16445  prdsgsumOLD  16446  dprd2d2  16517  gsumdixpOLD  16635  gsumdixp  16636  ptbasfi  18996  ptcnplem  19036  ptcnp  19037  cnmptk2  19101  cnmpt2k  19103  xkocnv  19229  fsumcn  20288  itg2cnlem1  21081  nfitg  21094  itgfsum  21146  dvmptfsum  21289  mpfrcl  21370  itgulm2  21759  fmptcof2  25803  fpwrelmap  25858  lgamgulm2  26870  nfcprod1  27270  nfcprod  27271  aomclem8  29259  refsum2cn  29605  fmuldfeq  29609  stoweidlem26  29667  stoweidlem31  29672  stoweidlem34  29675  stoweidlem35  29676  stoweidlem42  29683  stoweidlem48  29689  stoweidlem59  29700  ovmpt3rab1  30007  bnj1366  31546  cdleme32d  33682  cdleme32f  33684  cdlemksv2  34085  cdlemkuv2  34105  hlhilset  35176
  Copyright terms: Public domain W3C validator