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

Theorem nfmpt 5021
Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
Hypotheses
Ref Expression
nfmpt.1 𝑥𝐴
nfmpt.2 𝑥𝐵
Assertion
Ref Expression
nfmpt 𝑥(𝑦𝐴𝐵)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem nfmpt
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-mpt 5006 . 2 (𝑦𝐴𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐵)}
2 nfmpt.1 . . . . 5 𝑥𝐴
32nfcri 2921 . . . 4 𝑥 𝑦𝐴
4 nfmpt.2 . . . . 5 𝑥𝐵
54nfeq2 2942 . . . 4 𝑥 𝑧 = 𝐵
63, 5nfan 1863 . . 3 𝑥(𝑦𝐴𝑧 = 𝐵)
76nfopab 4994 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐵)}
81, 7nfcxfr 2925 1 𝑥(𝑦𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 387   = wceq 1508  wcel 2051  wnfc 2911  {copab 4988  cmpt 5005
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-opab 4989  df-mpt 5006
This theorem is referenced by:  ovmpt3rab1  7220  nfof  7231  mpocurryvald  7738  nfrdg  7853  mapxpen  8478  nfoi  8772  seqof2  13242  nfsum1  14906  nfsum  14907  fsumrlim  15025  fsumo1  15026  nfcprod1  15123  nfcprod  15124  gsum2d2  18860  prdsgsum  18864  dprd2d2  18929  gsumdixp  19095  mpfrcl  20024  ptbasfi  21909  ptcnplem  21949  ptcnp  21950  cnmptk2  22014  cnmpt2k  22016  xkocnv  22142  fsumcn  23197  itg2cnlem1  24081  nfitg  24094  itgfsum  24146  dvmptfsum  24291  itgulm2  24716  lgamgulm2  25331  fmptcof2  30182  fpwrelmap  30246  nfesum2  30977  sigapildsys  31099  oms0  31233  bnj1366  31782  nosupbnd2  32770  exrecfnlem  34135  poimirlem26  34392  cdleme32d  37058  cdleme32f  37060  cdlemksv2  37461  cdlemkuv2  37481  hlhilset  38548  aomclem8  39091  binomcxplemdvsum  40137  refsum2cn  40748  fmuldfeq  41325  fprodcnlem  41341  fprodcn  41342  fnlimfv  41405  fnlimcnv  41409  fnlimfvre  41416  fnlimfvre2  41419  fnlimf  41420  fnlimabslt  41421  fprodcncf  41644  dvnmptdivc  41683  dvmptfprod  41690  dvnprodlem1  41691  stoweidlem26  41772  stoweidlem31  41777  stoweidlem34  41780  stoweidlem35  41781  stoweidlem42  41788  stoweidlem48  41794  stoweidlem59  41805  fourierdlem31  41884  fourierdlem112  41964  sge0iunmptlemfi  42156  sge0iunmptlemre  42158  sge0iunmpt  42161  hoicvrrex  42299  ovncvrrp  42307  ovnhoilem1  42344  ovnlecvr2  42353  vonicc  42428  smflim  42514  smfmullem4  42530  smflim2  42541  smflimmpt  42545  smfsup  42549  smfsupmpt  42550  smfinf  42553  smfinfmpt  42554  smflimsuplem2  42556  smflimsuplem5  42559  smflimsup  42563  smflimsupmpt  42564  smfliminf  42566  smfliminfmpt  42567  aacllem  44299
  Copyright terms: Public domain W3C validator