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

Theorem nfmpt22 6708
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 6640 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 nfoprab2 6690 . 2 𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
31, 2nfcxfr 2760 1 𝑦(𝑥𝐴, 𝑦𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1481  wcel 1988  wnfc 2749  {coprab 6636  cmpt2 6637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-oprab 6639  df-mpt2 6640
This theorem is referenced by:  ovmpt2s  6769  ov2gf  6770  ovmpt2dxf  6771  ovmpt2df  6777  ovmpt2dv2  6779  xpcomco  8035  mapxpen  8111  pwfseqlem2  9466  pwfseqlem4a  9468  pwfseqlem4  9469  gsum2d2lem  18353  gsum2d2  18354  gsumcom2  18355  dprd2d2  18424  cnmpt21  21455  cnmpt2t  21457  cnmptcom  21462  cnmpt2k  21472  xkocnv  21598  finxpreclem2  33198  finxpreclem6  33204  fmuldfeq  39615  smflimlem6  40747  ovmpt2rdxf  41882
  Copyright terms: Public domain W3C validator