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

Theorem nfmpt21 6141
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 6087 . 2  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
2 nfoprab1 6124 . 2  |-  F/_ x { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
31, 2nfcxfr 2570 1  |-  F/_ x
( x  e.  A ,  y  e.  B  |->  C )
Colors of variables: wff set class
Syntax hints:    /\ wa 360    = wceq 1653    e. wcel 1726   F/_wnfc 2560   {coprab 6083    e. cmpt2 6084
This theorem is referenced by:  ovmpt2s  6198  ov2gf  6199  ovmpt2dxf  6200  ovmpt2df  6206  ovmpt2dv2  6208  xpcomco  7199  mapxpen  7274  pwfseqlem2  8535  pwfseqlem4a  8537  pwfseqlem4  8538  gsum2d2lem  15548  gsum2d2  15549  gsumcom2  15550  dprd2d2  15603  cnmpt21  17704  cnmpt2t  17706  cnmptcom  17711  cnmpt2k  17721  xkocnv  17847  fmuldfeqlem1  27689  fmuldfeq  27690
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-oprab 6086  df-mpt2 6087
  Copyright terms: Public domain W3C validator