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

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

Proof of Theorem nfmpt22
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-mpt2 6695 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 nfoprab2 6747 . 2 𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
31, 2nfcxfr 2791 1 𝑦(𝑥𝐴, 𝑦𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1523  wcel 2030  wnfc 2780  {coprab 6691  cmpt2 6692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-oprab 6694  df-mpt2 6695
This theorem is referenced by:  ovmpt2s  6826  ov2gf  6827  ovmpt2dxf  6828  ovmpt2df  6834  ovmpt2dv2  6836  xpcomco  8091  mapxpen  8167  pwfseqlem2  9519  pwfseqlem4a  9521  pwfseqlem4  9522  gsum2d2lem  18418  gsum2d2  18419  gsumcom2  18420  dprd2d2  18489  cnmpt21  21522  cnmpt2t  21524  cnmptcom  21529  cnmpt2k  21539  xkocnv  21665  finxpreclem2  33357  finxpreclem6  33363  fmuldfeq  40133  smflimlem6  41305  ovmpt2rdxf  42442
  Copyright terms: Public domain W3C validator