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

Theorem nfmpt21 5930
Description: Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
Assertion
Ref Expression
nfmpt21  |-  F/_ x
( x  e.  A ,  y  e.  B  |->  C )

Proof of Theorem nfmpt21
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 df-mpt2 5879 . 2  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
2 nfoprab1 5913 . 2  |-  F/_ x { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
31, 2nfcxfr 2429 1  |-  F/_ x
( x  e.  A ,  y  e.  B  |->  C )
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1632    e. wcel 1696   F/_wnfc 2419   {coprab 5875    e. cmpt2 5876
This theorem is referenced by:  ovmpt2s  5987  ov2gf  5988  ovmpt2dxf  5989  ovmpt2df  5995  ovmpt2dv2  5997  xpcomco  6968  mapxpen  7043  pwfseqlem2  8297  pwfseqlem4a  8299  pwfseqlem4  8300  gsum2d2lem  15240  gsum2d2  15241  gsumcom2  15242  dprd2d2  15295  cnmpt21  17381  cnmpt2t  17383  cnmptcom  17388  cnmpt2k  17398  xkocnv  17521  fmuldfeqlem1  27815  fmuldfeq  27816
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-oprab 5878  df-mpt2 5879
  Copyright terms: Public domain W3C validator