Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfmpo1 Structured version   Visualization version   GIF version

Theorem nfmpo1 7229
 Description: Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
Assertion
Ref Expression
nfmpo1 𝑥(𝑥𝐴, 𝑦𝐵𝐶)

Proof of Theorem nfmpo1
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-mpo 7156 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 nfoprab1 7210 . 2 𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
31, 2nfcxfr 2979 1 𝑥(𝑥𝐴, 𝑦𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 396   = wceq 1530   ∈ wcel 2106  Ⅎwnfc 2965  {coprab 7152   ∈ cmpo 7153 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-oprab 7155  df-mpo 7156 This theorem is referenced by:  ovmpos  7291  ov2gf  7292  ovmpodxf  7293  ovmpodf  7299  ovmpodv2  7301  xpcomco  8599  mapxpen  8675  pwfseqlem2  10073  pwfseqlem4a  10075  pwfseqlem4  10076  gsum2d2lem  19015  gsum2d2  19016  gsumcom2  19017  dprd2d2  19088  cnmpt21  22195  cnmpt2t  22197  cnmptcom  22202  cnmpt2k  22212  xkocnv  22338  numclwlk2lem2f1o  28073  finxpreclem2  34541  fmuldfeqlem1  41725  fmuldfeq  41726  ovmpordxf  44216
 Copyright terms: Public domain W3C validator