Theorem nfmpt 5208

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Ⅎwnfc 2877  {copab 5172   ↦ cmpt 5191

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-opab 5173  df-mpt 5192

This theorem is referenced by:  ovmpt3rab1  7650  nfof  7662  mpocurryvald  8252  nfrdg  8385  mapxpen  9113  nfoi  9474  seqof2  14032  nfsum1  15663  nfsum  15664  fsumrlim  15784  fsumo1  15785  nfcprod1  15881  nfcprod  15882  gsum2d2  19911  prdsgsum  19918  dprd2d2  19983  gsumdixp  20235  mpfrcl  21999  ptbasfi  23475  ptcnplem  23515  ptcnp  23516  cnmptk2  23580  cnmpt2k  23582  xkocnv  23708  fsumcn  24768  itg2cnlem1  25669  nfitg  25683  itgfsum  25735  dvmptfsum  25886  itgulm2  26325  lgamgulm2  26953  nosupbnd2  27635  noinfbnd2  27650  fmptcof2  32588  fpwrelmap  32663  nfesum2  34038  sigapildsys  34159  oms0  34295  bnj1366  34826  exrecfnlem  37374  poimirlem26  37647  cdleme32d  40445  cdleme32f  40447  cdlemksv2  40848  cdlemkuv2  40868  hlhilset  41935  pwsgprod  42539  aomclem8  43057  binomcxplemdvsum  44351  refsum2cn  45039  fmuldfeq  45588  fprodcnlem  45604  fprodcn  45605  fnlimfv  45668  fnlimcnv  45672  fnlimfvre  45679  fnlimfvre2  45682  fnlimf  45683  fnlimabslt  45684  fprodcncf  45905  dvnmptdivc  45943  dvmptfprod  45950  dvnprodlem1  45951  stoweidlem26  46031  stoweidlem31  46036  stoweidlem34  46039  stoweidlem35  46040  stoweidlem42  46047  stoweidlem48  46053  stoweidlem59  46064  fourierdlem31  46143  fourierdlem112  46223  sge0iunmptlemfi  46418  sge0iunmptlemre  46420  sge0iunmpt  46423  hoicvrrex  46561  ovncvrrp  46569  ovnhoilem1  46606  ovnlecvr2  46615  vonicc  46690  smflim  46782  smfmullem4  46799  smflim2  46811  smflimmpt  46815  smfsup  46819  smfsupmpt  46820  smfinf  46823  smfinfmpt  46824  smflimsuplem2  46826  smflimsuplem5  46829  smflimsup  46833  smflimsupmpt  46834  smfliminf  46836  smfliminfmpt  46837  fsupdm  46847  finfdm  46851  aacllem  49794