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

Theorem nfmpt21 6152
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 6095 . 2  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
2 nfoprab1 6134 . 2  |-  F/_ x { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
31, 2nfcxfr 2575 1  |-  F/_ x
( x  e.  A ,  y  e.  B  |->  C )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1369    e. wcel 1756   F/_wnfc 2565   {coprab 6091    e. cmpt2 6092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-oprab 6094  df-mpt2 6095
This theorem is referenced by:  ovmpt2s  6213  ov2gf  6214  ovmpt2dxf  6215  ovmpt2df  6221  ovmpt2dv2  6223  xpcomco  7400  mapxpen  7476  pwfseqlem2  8825  pwfseqlem4a  8827  pwfseqlem4  8828  gsum2d2lem  16464  gsum2d2  16465  gsumcom2  16466  dprd2d2  16542  cnmpt21  19243  cnmpt2t  19245  cnmptcom  19250  cnmpt2k  19260  xkocnv  19386  fmuldfeqlem1  29761  fmuldfeq  29762  ovmpt2rdxf  30727
  Copyright terms: Public domain W3C validator