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

Theorem nfmpt22 6338
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 6275 . 2  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
2 nfoprab2 6320 . 2  |-  F/_ y { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
31, 2nfcxfr 2614 1  |-  F/_ y
( x  e.  A ,  y  e.  B  |->  C )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 367    = wceq 1398    e. wcel 1823   F/_wnfc 2602   {coprab 6271    |-> cmpt2 6272
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-oprab 6274  df-mpt2 6275
This theorem is referenced by:  ovmpt2s  6399  ov2gf  6400  ovmpt2dxf  6401  ovmpt2df  6407  ovmpt2dv2  6409  xpcomco  7600  mapxpen  7676  pwfseqlem2  9026  pwfseqlem4a  9028  pwfseqlem4  9029  gsum2d2lem  17200  gsum2d2  17201  gsumcom2  17202  dprd2d2  17291  cnmpt21  20341  cnmpt2t  20343  cnmptcom  20348  cnmpt2k  20358  xkocnv  20484  fmuldfeq  31819  ovmpt2rdxf  33201
  Copyright terms: Public domain W3C validator