Theorem nfmpt 5219

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Ⅎwnfc 2883  {copab 5181   ↦ cmpt 5201

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-opab 5182  df-mpt 5202

This theorem is referenced by:  ovmpt3rab1  7665  nfof  7677  mpocurryvald  8269  nfrdg  8428  mapxpen  9157  nfoi  9528  seqof2  14078  nfsum1  15706  nfsum  15707  fsumrlim  15827  fsumo1  15828  nfcprod1  15924  nfcprod  15925  gsum2d2  19955  prdsgsum  19962  dprd2d2  20027  gsumdixp  20279  mpfrcl  22043  ptbasfi  23519  ptcnplem  23559  ptcnp  23560  cnmptk2  23624  cnmpt2k  23626  xkocnv  23752  fsumcn  24812  itg2cnlem1  25714  nfitg  25728  itgfsum  25780  dvmptfsum  25931  itgulm2  26370  lgamgulm2  26998  nosupbnd2  27680  noinfbnd2  27695  fmptcof2  32635  fpwrelmap  32710  nfesum2  34072  sigapildsys  34193  oms0  34329  bnj1366  34860  exrecfnlem  37397  poimirlem26  37670  cdleme32d  40463  cdleme32f  40465  cdlemksv2  40866  cdlemkuv2  40886  hlhilset  41953  pwsgprod  42567  aomclem8  43085  binomcxplemdvsum  44379  refsum2cn  45062  fmuldfeq  45612  fprodcnlem  45628  fprodcn  45629  fnlimfv  45692  fnlimcnv  45696  fnlimfvre  45703  fnlimfvre2  45706  fnlimf  45707  fnlimabslt  45708  fprodcncf  45929  dvnmptdivc  45967  dvmptfprod  45974  dvnprodlem1  45975  stoweidlem26  46055  stoweidlem31  46060  stoweidlem34  46063  stoweidlem35  46064  stoweidlem42  46071  stoweidlem48  46077  stoweidlem59  46088  fourierdlem31  46167  fourierdlem112  46247  sge0iunmptlemfi  46442  sge0iunmptlemre  46444  sge0iunmpt  46447  hoicvrrex  46585  ovncvrrp  46593  ovnhoilem1  46630  ovnlecvr2  46639  vonicc  46714  smflim  46806  smfmullem4  46823  smflim2  46835  smflimmpt  46839  smfsup  46843  smfsupmpt  46844  smfinf  46847  smfinfmpt  46848  smflimsuplem2  46850  smflimsuplem5  46853  smflimsup  46857  smflimsupmpt  46858  smfliminf  46860  smfliminfmpt  46861  fsupdm  46871  finfdm  46875  aacllem  49665