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

Theorem nfmpt 4491
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 4463 . 2  |-  ( y  e.  A  |->  B )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  B ) }
2 nfmpt.1 . . . . 5  |-  F/_ x A
32nfcri 2586 . . . 4  |-  F/ x  y  e.  A
4 nfmpt.2 . . . . 5  |-  F/_ x B
54nfeq2 2607 . . . 4  |-  F/ x  z  =  B
63, 5nfan 2011 . . 3  |-  F/ x
( y  e.  A  /\  z  =  B
)
76nfopab 4468 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  =  B ) }
81, 7nfcxfr 2590 1  |-  F/_ x
( y  e.  A  |->  B )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 371    = wceq 1444    e. wcel 1887   F/_wnfc 2579   {copab 4460    |-> cmpt 4461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-opab 4462  df-mpt 4463
This theorem is referenced by:  ovmpt3rab1  6525  mpt2curryvald  7017  nfrdg  7132  mapxpen  7738  nfoi  8029  seqof2  12271  nfsum1  13756  nfsum  13757  fsumrlim  13871  fsumo1  13872  nfcprod1  13964  nfcprod  13965  gsum2d2  17606  prdsgsum  17610  dprd2d2  17677  gsumdixp  17837  mpfrcl  18741  ptbasfi  20596  ptcnplem  20636  ptcnp  20637  cnmptk2  20701  cnmpt2k  20703  xkocnv  20829  fsumcn  21902  itg2cnlem1  22719  nfitg  22732  itgfsum  22784  dvmptfsum  22927  itgulm2  23364  lgamgulm2  23961  fmptcof2  28259  fpwrelmap  28318  nfesum2  28862  sigapildsys  28984  oms0  29125  oms0OLD  29129  bnj1366  29641  poimirlem26  31966  cdleme32d  34011  cdleme32f  34013  cdlemksv2  34414  cdlemkuv2  34434  hlhilset  35505  aomclem8  35919  binomcxplemdvsum  36704  refsum2cn  37359  wessf1ornlem  37459  fmuldfeq  37661  fprodcncf  37779  dvnmptdivc  37813  dvmptfprod  37820  dvnprodlem1  37821  stoweidlem26  37886  stoweidlem31  37892  stoweidlem34  37895  stoweidlem35  37896  stoweidlem42  37903  stoweidlem48  37909  stoweidlem59  37920  fourierdlem31  38000  fourierdlem31OLD  38001  fourierdlem112  38082  sge0iunmptlemfi  38255  sge0iunmptlemre  38257  sge0iunmpt  38260  hoicvrrex  38378  ovncvrrp  38386  ovnhoilem1  38423  ovnlecvr2  38432  aacllem  40593
  Copyright terms: Public domain W3C validator