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

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

Proof of Theorem nfmpt21
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-mpt2 6819 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 nfoprab1 6870 . 2 𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
31, 2nfcxfr 2900 1 𝑥(𝑥𝐴, 𝑦𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   = wceq 1632   ∈ wcel 2139  Ⅎwnfc 2889  {coprab 6815   ↦ cmpt2 6816 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-oprab 6818  df-mpt2 6819 This theorem is referenced by:  ovmpt2s  6950  ov2gf  6951  ovmpt2dxf  6952  ovmpt2df  6958  ovmpt2dv2  6960  xpcomco  8217  mapxpen  8293  pwfseqlem2  9693  pwfseqlem4a  9695  pwfseqlem4  9696  gsum2d2lem  18592  gsum2d2  18593  gsumcom2  18594  dprd2d2  18663  cnmpt21  21696  cnmpt2t  21698  cnmptcom  21703  cnmpt2k  21713  xkocnv  21839  numclwlk2lem2f1o  27561  numclwlk2lem2f1oOLD  27568  finxpreclem2  33556  cnfinltrel  33570  fmuldfeqlem1  40335  fmuldfeq  40336  ovmpt2rdxf  42645
 Copyright terms: Public domain W3C validator