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

Theorem nfmpt22 5915
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 5863 . 2  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
2 nfoprab2 5898 . 2  |-  F/_ y { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
31, 2nfcxfr 2416 1  |-  F/_ y
( x  e.  A ,  y  e.  B  |->  C )
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1623    e. wcel 1684   F/_wnfc 2406   {coprab 5859    e. cmpt2 5860
This theorem is referenced by:  ovmpt2s  5971  ov2gf  5972  ovmpt2dxf  5973  ovmpt2df  5979  ovmpt2dv2  5981  xpcomco  6952  mapxpen  7027  pwfseqlem2  8281  pwfseqlem4a  8283  pwfseqlem4  8284  gsum2d2lem  15224  gsum2d2  15225  gsumcom2  15226  dprd2d2  15279  cnmpt21  17365  cnmpt2t  17367  cnmptcom  17372  cnmpt2k  17382  xkocnv  17505  dya2iocrrnval  23582  fmuldfeq  27713
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-oprab 5862  df-mpt2 5863
  Copyright terms: Public domain W3C validator