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

Theorem nfmpt 4664
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 4635 . 2 (𝑦𝐴𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐵)}
2 nfmpt.1 . . . . 5 𝑥𝐴
32nfcri 2740 . . . 4 𝑥 𝑦𝐴
4 nfmpt.2 . . . . 5 𝑥𝐵
54nfeq2 2761 . . . 4 𝑥 𝑧 = 𝐵
63, 5nfan 1814 . . 3 𝑥(𝑦𝐴𝑧 = 𝐵)
76nfopab 4640 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐵)}
81, 7nfcxfr 2744 1 𝑥(𝑦𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wcel 1975  wnfc 2733  {copab 4632  cmpt 4633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-opab 4634  df-mpt 4635
This theorem is referenced by:  ovmpt3rab1  6762  mpt2curryvald  7256  nfrdg  7370  mapxpen  7984  nfoi  8275  seqof2  12672  nfsum1  14210  nfsum  14211  fsumrlim  14326  fsumo1  14327  nfcprod1  14421  nfcprod  14422  gsum2d2  18138  prdsgsum  18142  dprd2d2  18208  gsumdixp  18374  mpfrcl  19281  ptbasfi  21132  ptcnplem  21172  ptcnp  21173  cnmptk2  21237  cnmpt2k  21239  xkocnv  21365  fsumcn  22408  itg2cnlem1  23247  nfitg  23260  itgfsum  23312  dvmptfsum  23455  itgulm2  23880  lgamgulm2  24475  fmptcof2  28641  fpwrelmap  28698  nfesum2  29232  sigapildsys  29354  oms0  29488  bnj1366  29956  poimirlem26  32404  cdleme32d  34549  cdleme32f  34551  cdlemksv2  34952  cdlemkuv2  34972  hlhilset  36043  aomclem8  36448  binomcxplemdvsum  37375  refsum2cn  38019  wessf1ornlem  38165  fmuldfeq  38450  fprodcnlem  38466  fprodcn  38467  fnlimfv  38530  fnlimcnv  38534  fnlimfvre  38541  fnlimfvre2  38544  fnlimf  38545  fnlimabslt  38546  fprodcncf  38587  dvnmptdivc  38628  dvmptfprod  38635  dvnprodlem1  38636  stoweidlem26  38719  stoweidlem31  38724  stoweidlem34  38727  stoweidlem35  38728  stoweidlem42  38735  stoweidlem48  38741  stoweidlem59  38752  fourierdlem31  38831  fourierdlem112  38911  sge0iunmptlemfi  39106  sge0iunmptlemre  39108  sge0iunmpt  39111  hoicvrrex  39246  ovncvrrp  39254  ovnhoilem1  39291  ovnlecvr2  39300  vonicc  39376  smflim  39463  smfmullem4  39479  aacllem  42315
  Copyright terms: Public domain W3C validator