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

Theorem nfmpt 5150
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 5134 . 2 (𝑦𝐴𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐵)}
2 nfmpt.1 . . . . 5 𝑥𝐴
32nfcri 2969 . . . 4 𝑥 𝑦𝐴
4 nfmpt.2 . . . . 5 𝑥𝐵
54nfeq2 2999 . . . 4 𝑥 𝑧 = 𝐵
63, 5nfan 1901 . . 3 𝑥(𝑦𝐴𝑧 = 𝐵)
76nfopab 5121 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐵)}
81, 7nfcxfr 2980 1 𝑥(𝑦𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 399   = wceq 1538  wcel 2115  wnfc 2962  {copab 5115  cmpt 5133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-opab 5116  df-mpt 5134
This theorem is referenced by:  ovmpt3rab1  7399  nfof  7410  mpocurryvald  7934  nfrdg  8048  mapxpen  8682  nfoi  8977  seqof2  13435  nfsum1  15048  nfsum  15049  nfsumOLD  15050  fsumrlim  15168  fsumo1  15169  nfcprod1  15266  nfcprod  15267  gsum2d2  19096  prdsgsum  19103  dprd2d2  19168  gsumdixp  19364  mpfrcl  20766  ptbasfi  22195  ptcnplem  22235  ptcnp  22236  cnmptk2  22300  cnmpt2k  22302  xkocnv  22428  fsumcn  23484  itg2cnlem1  24374  nfitg  24387  itgfsum  24439  dvmptfsum  24587  itgulm2  25013  lgamgulm2  25630  fmptcof2  30421  fpwrelmap  30490  nfesum2  31385  sigapildsys  31506  oms0  31640  bnj1366  32186  nosupbnd2  33301  exrecfnlem  34768  poimirlem26  35055  cdleme32d  37712  cdleme32f  37714  cdlemksv2  38115  cdlemkuv2  38135  hlhilset  39202  aomclem8  39949  binomcxplemdvsum  41007  refsum2cn  41615  fmuldfeq  42178  fprodcnlem  42194  fprodcn  42195  fnlimfv  42258  fnlimcnv  42262  fnlimfvre  42269  fnlimfvre2  42272  fnlimf  42273  fnlimabslt  42274  fprodcncf  42495  dvnmptdivc  42533  dvmptfprod  42540  dvnprodlem1  42541  stoweidlem26  42621  stoweidlem31  42626  stoweidlem34  42629  stoweidlem35  42630  stoweidlem42  42637  stoweidlem48  42643  stoweidlem59  42654  fourierdlem31  42733  fourierdlem112  42813  sge0iunmptlemfi  43005  sge0iunmptlemre  43007  sge0iunmpt  43010  hoicvrrex  43148  ovncvrrp  43156  ovnhoilem1  43193  ovnlecvr2  43202  vonicc  43277  smflim  43363  smfmullem4  43379  smflim2  43390  smflimmpt  43394  smfsup  43398  smfsupmpt  43399  smfinf  43402  smfinfmpt  43403  smflimsuplem2  43405  smflimsuplem5  43408  smflimsup  43412  smflimsupmpt  43413  smfliminf  43415  smfliminfmpt  43416  aacllem  45282
  Copyright terms: Public domain W3C validator