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

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

Proof of Theorem nfmpt22
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 df-mpt2 6200 . 2  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
2 nfoprab2 6240 . 2  |-  F/_ y { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
31, 2nfcxfr 2612 1  |-  F/_ y
( x  e.  A ,  y  e.  B  |->  C )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1370    e. wcel 1758   F/_wnfc 2600   {coprab 6196    |-> cmpt2 6197
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-oprab 6199  df-mpt2 6200
This theorem is referenced by:  ovmpt2s  6319  ov2gf  6320  ovmpt2dxf  6321  ovmpt2df  6327  ovmpt2dv2  6329  xpcomco  7506  mapxpen  7582  pwfseqlem2  8932  pwfseqlem4a  8934  pwfseqlem4  8935  gsum2d2lem  16582  gsum2d2  16583  gsumcom2  16584  dprd2d2  16660  cnmpt21  19371  cnmpt2t  19373  cnmptcom  19378  cnmpt2k  19388  xkocnv  19514  fmuldfeq  29907  ovmpt2rdxf  30872
  Copyright terms: Public domain W3C validator