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

Theorem nfmpt 4375
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 4347 . 2  |-  ( y  e.  A  |->  B )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  B ) }
2 nfmpt.1 . . . . 5  |-  F/_ x A
32nfcri 2568 . . . 4  |-  F/ x  y  e.  A
4 nfmpt.2 . . . . 5  |-  F/_ x B
54nfeq2 2585 . . . 4  |-  F/ x  z  =  B
63, 5nfan 1860 . . 3  |-  F/ x
( y  e.  A  /\  z  =  B
)
76nfopab 4352 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  =  B ) }
81, 7nfcxfr 2571 1  |-  F/_ x
( y  e.  A  |->  B )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1369    e. wcel 1756   F/_wnfc 2561   {copab 4344    e. cmpt 4345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-opab 4346  df-mpt 4347
This theorem is referenced by:  nfrdg  6862  mapxpen  7469  nfoi  7720  seqof2  11856  nfsum1  13159  nfsum  13160  fsumrlim  13266  fsumo1  13267  gsum2d2  16454  prdsgsum  16459  prdsgsumOLD  16460  dprd2d2  16531  gsumdixpOLD  16688  gsumdixp  16689  mpfrcl  17579  ptbasfi  19129  ptcnplem  19169  ptcnp  19170  cnmptk2  19234  cnmpt2k  19236  xkocnv  19362  fsumcn  20421  itg2cnlem1  21214  nfitg  21227  itgfsum  21279  dvmptfsum  21422  itgulm2  21849  fmptcof2  25930  fpwrelmap  25984  oms0  26662  lgamgulm2  26974  nfcprod1  27374  nfcprod  27375  aomclem8  29367  refsum2cn  29713  fmuldfeq  29717  stoweidlem26  29774  stoweidlem31  29779  stoweidlem34  29782  stoweidlem35  29783  stoweidlem42  29790  stoweidlem48  29796  stoweidlem59  29807  ovmpt3rab1  30114  bnj1366  31710  cdleme32d  33928  cdleme32f  33930  cdlemksv2  34331  cdlemkuv2  34351  hlhilset  35422
  Copyright terms: Public domain W3C validator