Theorem nfmpt 5210

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.

Step	Hyp	Ref	Expression
1		df-mpt 5194	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2917	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2942	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1929	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 5181	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2923	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 400   = wceq 1570   ∈ wcel 2143  Ⅎwnfc 2910  {copab 5174   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-opab 5175  df-mpt 5194

This theorem is referenced by:  ovmpt3rab1  7670  nfof  7682  mpocurryvald  8267  nfrdg  8402  mapxpen  9132  nfoi  9477  seqof2  14098  nfsum1  15743  nfsum  15744  fsumrlim  15865  fsumo1  15866  nfcprod1  15964  nfcprod  15965  gsum2d2  20045  prdsgsum  20052  dprd2d2  20117  gsumdixp  20401  pwsgprod  20412  mpfrcl  22217  ptbasfi  23719  ptcnplem  23759  ptcnp  23760  cnmptk2  23824  cnmpt2k  23826  xkocnv  23952  fsumcn  25010  itg2cnlem1  25901  nfitg  25915  itgfsum  25967  dvmptfsum  26115  itgulm2  26553  lgamgulm2  27181  nosupbnd2  27861  noinfbnd2  27876  fmptcof2  32983  fpwrelmap  33059  nfesum2  34412  sigapildsys  34533  oms0  34668  bnj1366  35198  exrecfnlem  38006  poimirlem26  38278  cdleme32d  41199  cdleme32f  41201  cdlemksv2  41602  cdlemkuv2  41622  hlhilset  42689  aomclem8  43771  binomcxplemdvsum  45048  refsum2cn  45741  fmuldfeq  46282  fprodcnlem  46298  fprodcn  46299  fnlimfv  46360  fnlimcnv  46364  fnlimfvre  46371  fnlimfvre2  46374  fnlimf  46375  fnlimabslt  46376  fprodcncf  46597  dvnmptdivc  46635  dvmptfprod  46642  dvnprodlem1  46643  stoweidlem26  46723  stoweidlem31  46728  stoweidlem34  46731  stoweidlem35  46732  stoweidlem42  46739  stoweidlem48  46745  stoweidlem59  46756  fourierdlem31  46835  fourierdlem112  46915  sge0iunmptlemfi  47110  sge0iunmptlemre  47112  sge0iunmpt  47115  hoicvrrex  47253  ovncvrrp  47261  ovnhoilem1  47298  ovnlecvr2  47307  vonicc  47382  smflim  47474  smfmullem4  47491  smflim2  47503  smflimmpt  47507  smfsup  47511  smfsupmpt  47512  smfinf  47515  smfinfmpt  47516  smflimsuplem2  47518  smflimsuplem5  47521  smflimsup  47525  smflimsupmpt  47526  smfliminf  47528  smfliminfmpt  47529  fsupdm  47539  finfdm  47543  aacllem  50584