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

Theorem nfmpt 4487
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 4459 . 2  |-  ( y  e.  A  |->  B )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  B ) }
2 nfmpt.1 . . . . 5  |-  F/_ x A
32nfcri 2609 . . . 4  |-  F/ x  y  e.  A
4 nfmpt.2 . . . . 5  |-  F/_ x B
54nfeq2 2632 . . . 4  |-  F/ x  z  =  B
63, 5nfan 1866 . . 3  |-  F/ x
( y  e.  A  /\  z  =  B
)
76nfopab 4464 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  =  B ) }
81, 7nfcxfr 2614 1  |-  F/_ x
( y  e.  A  |->  B )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1370    e. wcel 1758   F/_wnfc 2602   {copab 4456    |-> cmpt 4457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-opab 4458  df-mpt 4459
This theorem is referenced by:  mpt2curryvald  6898  nfrdg  6979  mapxpen  7586  nfoi  7838  seqof2  11980  nfsum1  13284  nfsum  13285  fsumrlim  13391  fsumo1  13392  gsum2d2  16587  prdsgsum  16592  prdsgsumOLD  16593  dprd2d2  16664  gsumdixpOLD  16822  gsumdixp  16823  mpfrcl  17727  ptbasfi  19285  ptcnplem  19325  ptcnp  19326  cnmptk2  19390  cnmpt2k  19392  xkocnv  19518  fsumcn  20577  itg2cnlem1  21371  nfitg  21384  itgfsum  21436  dvmptfsum  21579  itgulm2  22006  fmptcof2  26129  fpwrelmap  26183  oms0  26853  lgamgulm2  27165  nfcprod1  27566  nfcprod  27567  aomclem8  29561  refsum2cn  29907  fmuldfeq  29911  stoweidlem26  29968  stoweidlem31  29973  stoweidlem34  29976  stoweidlem35  29977  stoweidlem42  29984  stoweidlem48  29990  stoweidlem59  30001  ovmpt3rab1  30308  bnj1366  32140  cdleme32d  34411  cdleme32f  34413  cdlemksv2  34814  cdlemkuv2  34834  hlhilset  35905
  Copyright terms: Public domain W3C validator