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

Theorem nfmpo2 7433
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 7357 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 nfoprab2 7414 . 2 𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
31, 2nfcxfr 2904 1 𝑦(𝑥𝐴, 𝑦𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wa 397   = wceq 1542  wcel 2107  wnfc 2886  {coprab 7353  cmpo 7354
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 2709
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 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-oprab 7356  df-mpo 7357
This theorem is referenced by:  ovmpos  7498  ov2gf  7499  ovmpodxf  7500  ovmpodf  7506  ovmpodv2  7508  xpcomco  8965  mapxpen  9046  pwfseqlem2  10554  pwfseqlem4a  10556  pwfseqlem4  10557  gsum2d2lem  19709  gsum2d2  19710  gsumcom2  19711  dprd2d2  19782  cnmpt21  22974  cnmpt2t  22976  cnmptcom  22981  cnmpt2k  22991  xkocnv  23117  finxpreclem2  35793  finxpreclem6  35799  mnringmulrcld  42413  fmuldfeq  43719  smflimlem6  44912  ovmpordxf  46309
  Copyright terms: Public domain W3C validator