Theorem nfmpt 5193

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 5177	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2883	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2909	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1899	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 5164	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2889	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Ⅎwnfc 2876  {copab 5157   ↦ cmpt 5176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-opab 5158  df-mpt 5177

This theorem is referenced by:  ovmpt3rab1  7611  nfof  7623  mpocurryvald  8210  nfrdg  8343  mapxpen  9067  nfoi  9425  seqof2  13986  nfsum1  15616  nfsum  15617  fsumrlim  15737  fsumo1  15738  nfcprod1  15834  nfcprod  15835  gsum2d2  19872  prdsgsum  19879  dprd2d2  19944  gsumdixp  20223  mpfrcl  22009  ptbasfi  23485  ptcnplem  23525  ptcnp  23526  cnmptk2  23590  cnmpt2k  23592  xkocnv  23718  fsumcn  24778  itg2cnlem1  25679  nfitg  25693  itgfsum  25745  dvmptfsum  25896  itgulm2  26335  lgamgulm2  26963  nosupbnd2  27645  noinfbnd2  27660  fmptcof2  32619  fpwrelmap  32695  nfesum2  34027  sigapildsys  34148  oms0  34284  bnj1366  34815  exrecfnlem  37372  poimirlem26  37645  cdleme32d  40443  cdleme32f  40445  cdlemksv2  40846  cdlemkuv2  40866  hlhilset  41933  pwsgprod  42537  aomclem8  43054  binomcxplemdvsum  44348  refsum2cn  45036  fmuldfeq  45584  fprodcnlem  45600  fprodcn  45601  fnlimfv  45664  fnlimcnv  45668  fnlimfvre  45675  fnlimfvre2  45678  fnlimf  45679  fnlimabslt  45680  fprodcncf  45901  dvnmptdivc  45939  dvmptfprod  45946  dvnprodlem1  45947  stoweidlem26  46027  stoweidlem31  46032  stoweidlem34  46035  stoweidlem35  46036  stoweidlem42  46043  stoweidlem48  46049  stoweidlem59  46060  fourierdlem31  46139  fourierdlem112  46219  sge0iunmptlemfi  46414  sge0iunmptlemre  46416  sge0iunmpt  46419  hoicvrrex  46557  ovncvrrp  46565  ovnhoilem1  46602  ovnlecvr2  46611  vonicc  46686  smflim  46778  smfmullem4  46795  smflim2  46807  smflimmpt  46811  smfsup  46815  smfsupmpt  46816  smfinf  46819  smfinfmpt  46820  smflimsuplem2  46822  smflimsuplem5  46825  smflimsup  46829  smflimsupmpt  46830  smfliminf  46832  smfliminfmpt  46833  fsupdm  46843  finfdm  46847  aacllem  49806