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

Theorem nfmpo1 7364
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 7289 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 nfoprab1 7345 . 2 𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
31, 2nfcxfr 2906 1 𝑥(𝑥𝐴, 𝑦𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1539  wcel 2107  wnfc 2888  {coprab 7285  cmpo 7286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-oprab 7288  df-mpo 7289
This theorem is referenced by:  ovmpos  7430  ov2gf  7431  ovmpodxf  7432  ovmpodf  7438  ovmpodv2  7440  xpcomco  8858  mapxpen  8939  pwfseqlem2  10424  pwfseqlem4a  10426  pwfseqlem4  10427  gsum2d2lem  19583  gsum2d2  19584  gsumcom2  19585  dprd2d2  19656  cnmpt21  22831  cnmpt2t  22833  cnmptcom  22838  cnmpt2k  22848  xkocnv  22974  numclwlk2lem2f1o  28752  finxpreclem2  35570  mnringmulrcld  41853  fmuldfeqlem1  43130  fmuldfeq  43131  ovmpordxf  45685
  Copyright terms: Public domain W3C validator