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

Theorem nfmpt 4545
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 4517 . 2  |-  ( y  e.  A  |->  B )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  B ) }
2 nfmpt.1 . . . . 5  |-  F/_ x A
32nfcri 2612 . . . 4  |-  F/ x  y  e.  A
4 nfmpt.2 . . . . 5  |-  F/_ x B
54nfeq2 2636 . . . 4  |-  F/ x  z  =  B
63, 5nfan 1929 . . 3  |-  F/ x
( y  e.  A  /\  z  =  B
)
76nfopab 4522 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  =  B ) }
81, 7nfcxfr 2617 1  |-  F/_ x
( y  e.  A  |->  B )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1395    e. wcel 1819   F/_wnfc 2605   {copab 4514    |-> cmpt 4515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-opab 4516  df-mpt 4517
This theorem is referenced by:  ovmpt3rab1  6533  mpt2curryvald  7017  nfrdg  7098  mapxpen  7702  nfoi  7957  seqof2  12167  nfsum1  13523  nfsum  13524  fsumrlim  13636  fsumo1  13637  nfcprod1  13728  nfcprod  13729  gsum2d2  17128  prdsgsum  17133  prdsgsumOLD  17134  dprd2d2  17219  gsumdixpOLD  17383  gsumdixp  17384  mpfrcl  18313  ptbasfi  20207  ptcnplem  20247  ptcnp  20248  cnmptk2  20312  cnmpt2k  20314  xkocnv  20440  fsumcn  21499  itg2cnlem1  22293  nfitg  22306  itgfsum  22358  dvmptfsum  22501  itgulm2  22929  fmptcof2  27645  fpwrelmap  27706  nfesum2  28207  oms0  28429  lgamgulm2  28753  aomclem8  31169  binomcxplemdvsum  31422  refsum2cn  31574  fmuldfeq  31738  fprodcncf  31865  dvnmptdivc  31896  dvmptfprod  31903  dvnprodlem1  31904  stoweidlem26  31969  stoweidlem31  31974  stoweidlem34  31977  stoweidlem35  31978  stoweidlem42  31985  stoweidlem48  31991  stoweidlem59  32002  fourierdlem31  32081  fourierdlem112  32162  aacllem  33318  bnj1366  33989  cdleme32d  36271  cdleme32f  36273  cdlemksv2  36674  cdlemkuv2  36694  hlhilset  37765
  Copyright terms: Public domain W3C validator