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

Theorem nfmpt 4484
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 4456 . 2  |-  ( y  e.  A  |->  B )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  B ) }
2 nfmpt.1 . . . . 5  |-  F/_ x A
32nfcri 2606 . . . 4  |-  F/ x  y  e.  A
4 nfmpt.2 . . . . 5  |-  F/_ x B
54nfeq2 2627 . . . 4  |-  F/ x  z  =  B
63, 5nfan 2031 . . 3  |-  F/ x
( y  e.  A  /\  z  =  B
)
76nfopab 4461 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  =  B ) }
81, 7nfcxfr 2610 1  |-  F/_ x
( y  e.  A  |->  B )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 376    = wceq 1452    e. wcel 1904   F/_wnfc 2599   {copab 4453    |-> cmpt 4454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-opab 4455  df-mpt 4456
This theorem is referenced by:  ovmpt3rab1  6544  mpt2curryvald  7035  nfrdg  7150  mapxpen  7756  nfoi  8047  seqof2  12309  nfsum1  13833  nfsum  13834  fsumrlim  13948  fsumo1  13949  nfcprod1  14041  nfcprod  14042  gsum2d2  17684  prdsgsum  17688  dprd2d2  17755  gsumdixp  17915  mpfrcl  18818  ptbasfi  20673  ptcnplem  20713  ptcnp  20714  cnmptk2  20778  cnmpt2k  20780  xkocnv  20906  fsumcn  21980  itg2cnlem1  22798  nfitg  22811  itgfsum  22863  dvmptfsum  23006  itgulm2  23443  lgamgulm2  24040  fmptcof2  28334  fpwrelmap  28393  nfesum2  28936  sigapildsys  29058  oms0  29198  oms0OLD  29202  bnj1366  29713  poimirlem26  32030  cdleme32d  34082  cdleme32f  34084  cdlemksv2  34485  cdlemkuv2  34505  hlhilset  35576  aomclem8  35990  binomcxplemdvsum  36774  refsum2cn  37422  wessf1ornlem  37530  fmuldfeq  37758  fprodcncf  37876  dvnmptdivc  37910  dvmptfprod  37917  dvnprodlem1  37918  stoweidlem26  37998  stoweidlem31  38004  stoweidlem34  38007  stoweidlem35  38008  stoweidlem42  38015  stoweidlem48  38021  stoweidlem59  38032  fourierdlem31  38112  fourierdlem31OLD  38113  fourierdlem112  38194  sge0iunmptlemfi  38369  sge0iunmptlemre  38371  sge0iunmpt  38374  hoicvrrex  38496  ovncvrrp  38504  ovnhoilem1  38541  ovnlecvr2  38550  aacllem  41046
  Copyright terms: Public domain W3C validator