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

Theorem nfmpo1 7514
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 7437 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 nfoprab1 7495 . 2 𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
31, 2nfcxfr 2902 1 𝑥(𝑥𝐴, 𝑦𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1539  wcel 2107  wnfc 2889  {coprab 7433  cmpo 7434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-oprab 7436  df-mpo 7437
This theorem is referenced by:  ovmpos  7582  ov2gf  7583  ovmpodxf  7584  ovmpodf  7590  ovmpodv2  7592  xpcomco  9103  mapxpen  9184  pwfseqlem2  10700  pwfseqlem4a  10702  pwfseqlem4  10703  gsum2d2lem  19992  gsum2d2  19993  gsumcom2  19994  dprd2d2  20065  cnmpt21  23680  cnmpt2t  23682  cnmptcom  23687  cnmpt2k  23697  xkocnv  23823  numclwlk2lem2f1o  30399  finxpreclem2  37392  mnringmulrcld  44252  fmuldfeqlem1  45602  fmuldfeq  45603  ovmpordxf  48260
  Copyright terms: Public domain W3C validator