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

Theorem nfmpt 4737
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 4721 . 2 (𝑦𝐴𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐵)}
2 nfmpt.1 . . . . 5 𝑥𝐴
32nfcri 2756 . . . 4 𝑥 𝑦𝐴
4 nfmpt.2 . . . . 5 𝑥𝐵
54nfeq2 2777 . . . 4 𝑥 𝑧 = 𝐵
63, 5nfan 1826 . . 3 𝑥(𝑦𝐴𝑧 = 𝐵)
76nfopab 4709 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐵)}
81, 7nfcxfr 2760 1 𝑥(𝑦𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1481  wcel 1988  wnfc 2749  {copab 4703  cmpt 4720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-opab 4704  df-mpt 4721
This theorem is referenced by:  ovmpt3rab1  6876  mpt2curryvald  7381  nfrdg  7495  mapxpen  8111  nfoi  8404  seqof2  12842  nfsum1  14401  nfsum  14402  fsumrlim  14524  fsumo1  14525  nfcprod1  14621  nfcprod  14622  gsum2d2  18354  prdsgsum  18358  dprd2d2  18424  gsumdixp  18590  mpfrcl  19499  ptbasfi  21365  ptcnplem  21405  ptcnp  21406  cnmptk2  21470  cnmpt2k  21472  xkocnv  21598  fsumcn  22654  itg2cnlem1  23509  nfitg  23522  itgfsum  23574  dvmptfsum  23719  itgulm2  24144  lgamgulm2  24743  fmptcof2  29430  fpwrelmap  29482  nfesum2  30077  sigapildsys  30199  oms0  30333  bnj1366  30874  nosupbnd2  31836  poimirlem26  33406  cdleme32d  35551  cdleme32f  35553  cdlemksv2  35954  cdlemkuv2  35974  hlhilset  37045  aomclem8  37450  binomcxplemdvsum  38374  refsum2cn  39017  wessf1ornlem  39187  fmuldfeq  39615  fprodcnlem  39631  fprodcn  39632  fnlimfv  39695  fnlimcnv  39699  fnlimfvre  39706  fnlimfvre2  39709  fnlimf  39710  fnlimabslt  39711  fprodcncf  39877  dvnmptdivc  39916  dvmptfprod  39923  dvnprodlem1  39924  stoweidlem26  40006  stoweidlem31  40011  stoweidlem34  40014  stoweidlem35  40015  stoweidlem42  40022  stoweidlem48  40028  stoweidlem59  40039  fourierdlem31  40118  fourierdlem112  40198  sge0iunmptlemfi  40393  sge0iunmptlemre  40395  sge0iunmpt  40398  hoicvrrex  40533  ovncvrrp  40541  ovnhoilem1  40578  ovnlecvr2  40587  vonicc  40662  smflim  40748  smfmullem4  40764  smflim2  40775  smflimmpt  40779  smfsup  40783  smfsupmpt  40784  smfinf  40787  smfinfmpt  40788  smflimsuplem2  40790  smflimsuplem5  40793  smflimsup  40797  smflimsupmpt  40798  smfliminf  40800  smfliminfmpt  40801  aacllem  42312
  Copyright terms: Public domain W3C validator