Theorem nfmpt 5021

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 5006	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2921	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2942	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1863	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 4994	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2925	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 387   = wceq 1508   ∈ wcel 2051  Ⅎwnfc 2911  {copab 4988   ↦ cmpt 5005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-opab 4989  df-mpt 5006

This theorem is referenced by:  ovmpt3rab1  7220  nfof  7231  mpocurryvald  7738  nfrdg  7853  mapxpen  8478  nfoi  8772  seqof2  13242  nfsum1  14906  nfsum  14907  fsumrlim  15025  fsumo1  15026  nfcprod1  15123  nfcprod  15124  gsum2d2  18860  prdsgsum  18864  dprd2d2  18929  gsumdixp  19095  mpfrcl  20024  ptbasfi  21909  ptcnplem  21949  ptcnp  21950  cnmptk2  22014  cnmpt2k  22016  xkocnv  22142  fsumcn  23197  itg2cnlem1  24081  nfitg  24094  itgfsum  24146  dvmptfsum  24291  itgulm2  24716  lgamgulm2  25331  fmptcof2  30182  fpwrelmap  30246  nfesum2  30977  sigapildsys  31099  oms0  31233  bnj1366  31782  nosupbnd2  32770  exrecfnlem  34135  poimirlem26  34392  cdleme32d  37058  cdleme32f  37060  cdlemksv2  37461  cdlemkuv2  37481  hlhilset  38548  aomclem8  39091  binomcxplemdvsum  40137  refsum2cn  40748  fmuldfeq  41325  fprodcnlem  41341  fprodcn  41342  fnlimfv  41405  fnlimcnv  41409  fnlimfvre  41416  fnlimfvre2  41419  fnlimf  41420  fnlimabslt  41421  fprodcncf  41644  dvnmptdivc  41683  dvmptfprod  41690  dvnprodlem1  41691  stoweidlem26  41772  stoweidlem31  41777  stoweidlem34  41780  stoweidlem35  41781  stoweidlem42  41788  stoweidlem48  41794  stoweidlem59  41805  fourierdlem31  41884  fourierdlem112  41964  sge0iunmptlemfi  42156  sge0iunmptlemre  42158  sge0iunmpt  42161  hoicvrrex  42299  ovncvrrp  42307  ovnhoilem1  42344  ovnlecvr2  42353  vonicc  42428  smflim  42514  smfmullem4  42530  smflim2  42541  smflimmpt  42545  smfsup  42549  smfsupmpt  42550  smfinf  42553  smfinfmpt  42554  smflimsuplem2  42556  smflimsuplem5  42559  smflimsup  42563  smflimsupmpt  42564  smfliminf  42566  smfliminfmpt  42567  aacllem  44299