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

Theorem nfmpt21 6922
 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 6849 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 nfoprab1 6904 . 2 𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
31, 2nfcxfr 2905 1 𝑥(𝑥𝐴, 𝑦𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 384   = wceq 1652   ∈ wcel 2155  Ⅎwnfc 2894  {coprab 6845   ↦ cmpt2 6846 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743 This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-oprab 6848  df-mpt2 6849 This theorem is referenced by:  ovmpt2s  6984  ov2gf  6985  ovmpt2dxf  6986  ovmpt2df  6992  ovmpt2dv2  6994  xpcomco  8259  mapxpen  8335  pwfseqlem2  9736  pwfseqlem4a  9738  pwfseqlem4  9739  gsum2d2lem  18641  gsum2d2  18642  gsumcom2  18643  dprd2d2  18713  cnmpt21  21757  cnmpt2t  21759  cnmptcom  21764  cnmpt2k  21774  xkocnv  21900  numclwlk2lem2f1o  27686  numclwlk2lem2f1oOLD  27689  numclwlk2lem2f1oOLDOLD  27697  finxpreclem2  33663  cnfinltrel  33677  fmuldfeqlem1  40455  fmuldfeq  40456  ovmpt2rdxf  42789
 Copyright terms: Public domain W3C validator