Theorem nfmpt 5183

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Ⅎwnfc 2883  {copab 5147   ↦ cmpt 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-opab 5148  df-mpt 5167

This theorem is referenced by:  ovmpt3rab1  7625  nfof  7637  mpocurryvald  8220  nfrdg  8353  mapxpen  9081  nfoi  9429  seqof2  14022  nfsum1  15652  nfsum  15653  fsumrlim  15774  fsumo1  15775  nfcprod1  15873  nfcprod  15874  gsum2d2  19949  prdsgsum  19956  dprd2d2  20021  gsumdixp  20298  pwsgprod  20309  mpfrcl  22063  ptbasfi  23546  ptcnplem  23586  ptcnp  23587  cnmptk2  23651  cnmpt2k  23653  xkocnv  23779  fsumcn  24837  itg2cnlem1  25728  nfitg  25742  itgfsum  25794  dvmptfsum  25942  itgulm2  26374  lgamgulm2  26999  nosupbnd2  27680  noinfbnd2  27695  fmptcof2  32730  fpwrelmap  32806  nfesum2  34185  sigapildsys  34306  oms0  34441  bnj1366  34971  exrecfnlem  37695  poimirlem26  37967  cdleme32d  40890  cdleme32f  40892  cdlemksv2  41293  cdlemkuv2  41313  hlhilset  42380  aomclem8  43489  binomcxplemdvsum  44782  refsum2cn  45469  fmuldfeq  46013  fprodcnlem  46029  fprodcn  46030  fnlimfv  46091  fnlimcnv  46095  fnlimfvre  46102  fnlimfvre2  46105  fnlimf  46106  fnlimabslt  46107  fprodcncf  46328  dvnmptdivc  46366  dvmptfprod  46373  dvnprodlem1  46374  stoweidlem26  46454  stoweidlem31  46459  stoweidlem34  46462  stoweidlem35  46463  stoweidlem42  46470  stoweidlem48  46476  stoweidlem59  46487  fourierdlem31  46566  fourierdlem112  46646  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0iunmpt  46846  hoicvrrex  46984  ovncvrrp  46992  ovnhoilem1  47029  ovnlecvr2  47038  vonicc  47113  smflim  47205  smfmullem4  47222  smflim2  47234  smflimmpt  47238  smfsup  47242  smfsupmpt  47243  smfinf  47246  smfinfmpt  47247  smflimsuplem2  47249  smflimsuplem5  47252  smflimsup  47256  smflimsupmpt  47257  smfliminf  47259  smfliminfmpt  47260  fsupdm  47270  finfdm  47274  aacllem  50276