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

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

Proof of Theorem nfmpo2
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-mpo 7414 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 nfoprab2 7471 . 2 𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
31, 2nfcxfr 2902 1 𝑦(𝑥𝐴, 𝑦𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wa 397   = wceq 1542  wcel 2107  wnfc 2884  {coprab 7410  cmpo 7411
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 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-oprab 7413  df-mpo 7414
This theorem is referenced by:  ovmpos  7556  ov2gf  7557  ovmpodxf  7558  ovmpodf  7564  ovmpodv2  7566  xpcomco  9062  mapxpen  9143  pwfseqlem2  10654  pwfseqlem4a  10656  pwfseqlem4  10657  gsum2d2lem  19841  gsum2d2  19842  gsumcom2  19843  dprd2d2  19914  cnmpt21  23175  cnmpt2t  23177  cnmptcom  23182  cnmpt2k  23192  xkocnv  23318  finxpreclem2  36271  finxpreclem6  36277  mnringmulrcld  42987  fmuldfeq  44299  smflimlem6  45492  ovmpordxf  47014
  Copyright terms: Public domain W3C validator