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

Theorem nfmpt 5256
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 5233 . 2 (𝑦𝐴𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐵)}
2 nfmpt.1 . . . . 5 𝑥𝐴
32nfcri 2882 . . . 4 𝑥 𝑦𝐴
4 nfmpt.2 . . . . 5 𝑥𝐵
54nfeq2 2909 . . . 4 𝑥 𝑧 = 𝐵
63, 5nfan 1894 . . 3 𝑥(𝑦𝐴𝑧 = 𝐵)
76nfopab 5218 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐵)}
81, 7nfcxfr 2889 1 𝑥(𝑦𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 394   = wceq 1533  wcel 2098  wnfc 2875  {copab 5211  cmpt 5232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-opab 5212  df-mpt 5233
This theorem is referenced by:  ovmpt3rab1  7679  nfof  7691  mpocurryvald  8276  nfrdg  8435  mapxpen  9168  nfoi  9539  seqof2  14061  nfsum1  15672  nfsum  15673  fsumrlim  15793  fsumo1  15794  nfcprod1  15890  nfcprod  15891  gsum2d2  19941  prdsgsum  19948  dprd2d2  20013  gsumdixp  20267  mpfrcl  22053  ptbasfi  23529  ptcnplem  23569  ptcnp  23570  cnmptk2  23634  cnmpt2k  23636  xkocnv  23762  fsumcn  24832  itg2cnlem1  25735  nfitg  25748  itgfsum  25800  dvmptfsum  25951  itgulm2  26390  lgamgulm2  27013  nosupbnd2  27695  noinfbnd2  27710  fmptcof2  32524  fpwrelmap  32597  nfesum2  33788  sigapildsys  33909  oms0  34045  bnj1366  34588  exrecfnlem  36986  poimirlem26  37247  cdleme32d  40044  cdleme32f  40046  cdlemksv2  40447  cdlemkuv2  40467  hlhilset  41534  pwsgprod  41909  aomclem8  42624  binomcxplemdvsum  43931  refsum2cn  44539  fmuldfeq  45106  fprodcnlem  45122  fprodcn  45123  fnlimfv  45186  fnlimcnv  45190  fnlimfvre  45197  fnlimfvre2  45200  fnlimf  45201  fnlimabslt  45202  fprodcncf  45423  dvnmptdivc  45461  dvmptfprod  45468  dvnprodlem1  45469  stoweidlem26  45549  stoweidlem31  45554  stoweidlem34  45557  stoweidlem35  45558  stoweidlem42  45565  stoweidlem48  45571  stoweidlem59  45582  fourierdlem31  45661  fourierdlem112  45741  sge0iunmptlemfi  45936  sge0iunmptlemre  45938  sge0iunmpt  45941  hoicvrrex  46079  ovncvrrp  46087  ovnhoilem1  46124  ovnlecvr2  46133  vonicc  46208  smflim  46300  smfmullem4  46317  smflim2  46329  smflimmpt  46333  smfsup  46337  smfsupmpt  46338  smfinf  46341  smfinfmpt  46342  smflimsuplem2  46344  smflimsuplem5  46347  smflimsup  46351  smflimsupmpt  46352  smfliminf  46354  smfliminfmpt  46355  fsupdm  46365  finfdm  46369  aacllem  48417
  Copyright terms: Public domain W3C validator