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

Theorem nfmpo2 7215
 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 7141 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 nfoprab2 7196 . 2 𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
31, 2nfcxfr 2953 1 𝑦(𝑥𝐴, 𝑦𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Ⅎwnfc 2936  {coprab 7137   ∈ cmpo 7138 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-oprab 7140  df-mpo 7141 This theorem is referenced by:  ovmpos  7279  ov2gf  7280  ovmpodxf  7281  ovmpodf  7287  ovmpodv2  7289  xpcomco  8593  mapxpen  8670  pwfseqlem2  10073  pwfseqlem4a  10075  pwfseqlem4  10076  gsum2d2lem  19090  gsum2d2  19091  gsumcom2  19092  dprd2d2  19163  cnmpt21  22286  cnmpt2t  22288  cnmptcom  22293  cnmpt2k  22303  xkocnv  22429  finxpreclem2  34826  finxpreclem6  34832  mnringmulrcld  40979  fmuldfeq  42268  smflimlem6  43452  ovmpordxf  44783
 Copyright terms: Public domain W3C validator