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  13985  nfsum1  15615  nfsum  15616  fsumrlim  15736  fsumo1  15737  nfcprod1  15833  nfcprod  15834  gsum2d2  19871  prdsgsum  19878  dprd2d2  19943  gsumdixp  20222  mpfrcl  22008  ptbasfi  23484  ptcnplem  23524  ptcnp  23525  cnmptk2  23589  cnmpt2k  23591  xkocnv  23717  fsumcn  24777  itg2cnlem1  25678  nfitg  25692  itgfsum  25744  dvmptfsum  25895  itgulm2  26334  lgamgulm2  26962  nosupbnd2  27644  noinfbnd2  27659  fmptcof2  32614  fpwrelmap  32689  nfesum2  34010  sigapildsys  34131  oms0  34267  bnj1366  34798  exrecfnlem  37355  poimirlem26  37628  cdleme32d  40426  cdleme32f  40428  cdlemksv2  40829  cdlemkuv2  40849  hlhilset  41916  pwsgprod  42520  aomclem8  43037  binomcxplemdvsum  44331  refsum2cn  45019  fmuldfeq  45568  fprodcnlem  45584  fprodcn  45585  fnlimfv  45648  fnlimcnv  45652  fnlimfvre  45659  fnlimfvre2  45662  fnlimf  45663  fnlimabslt  45664  fprodcncf  45885  dvnmptdivc  45923  dvmptfprod  45930  dvnprodlem1  45931  stoweidlem26  46011  stoweidlem31  46016  stoweidlem34  46019  stoweidlem35  46020  stoweidlem42  46027  stoweidlem48  46033  stoweidlem59  46044  fourierdlem31  46123  fourierdlem112  46203  sge0iunmptlemfi  46398  sge0iunmptlemre  46400  sge0iunmpt  46403  hoicvrrex  46541  ovncvrrp  46549  ovnhoilem1  46586  ovnlecvr2  46595  vonicc  46670  smflim  46762  smfmullem4  46779  smflim2  46791  smflimmpt  46795  smfsup  46799  smfsupmpt  46800  smfinf  46803  smfinfmpt  46804  smflimsuplem2  46806  smflimsuplem5  46809  smflimsup  46813  smflimsupmpt  46814  smfliminf  46816  smfliminfmpt  46817  fsupdm  46827  finfdm  46831  aacllem  49790