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

Theorem nfmpo2 7513
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 7435 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 nfoprab2 7494 . 2 𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
31, 2nfcxfr 2900 1 𝑦(𝑥𝐴, 𝑦𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1536  wcel 2105  wnfc 2887  {coprab 7431  cmpo 7432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-oprab 7434  df-mpo 7435
This theorem is referenced by:  ovmpos  7580  ov2gf  7581  ovmpodxf  7582  ovmpodf  7588  ovmpodv2  7590  xpcomco  9100  mapxpen  9181  pwfseqlem2  10696  pwfseqlem4a  10698  pwfseqlem4  10699  gsum2d2lem  20005  gsum2d2  20006  gsumcom2  20007  dprd2d2  20078  cnmpt21  23694  cnmpt2t  23696  cnmptcom  23701  cnmpt2k  23711  xkocnv  23837  finxpreclem2  37372  finxpreclem6  37378  mnringmulrcld  44223  fmuldfeq  45538  smflimlem6  46731  ovmpordxf  48183
  Copyright terms: Public domain W3C validator