Theorem nfmpt 5196

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Ⅎwnfc 2883  {copab 5160   ↦ cmpt 5179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-opab 5161  df-mpt 5180

This theorem is referenced by:  ovmpt3rab1  7616  nfof  7628  mpocurryvald  8212  nfrdg  8345  mapxpen  9071  nfoi  9419  seqof2  13983  nfsum1  15613  nfsum  15614  fsumrlim  15734  fsumo1  15735  nfcprod1  15831  nfcprod  15832  gsum2d2  19903  prdsgsum  19910  dprd2d2  19975  gsumdixp  20254  pwsgprod  20265  mpfrcl  22040  ptbasfi  23525  ptcnplem  23565  ptcnp  23566  cnmptk2  23630  cnmpt2k  23632  xkocnv  23758  fsumcn  24817  itg2cnlem1  25718  nfitg  25732  itgfsum  25784  dvmptfsum  25935  itgulm2  26374  lgamgulm2  27002  nosupbnd2  27684  noinfbnd2  27699  fmptcof2  32735  fpwrelmap  32812  nfesum2  34198  sigapildsys  34319  oms0  34454  bnj1366  34985  exrecfnlem  37584  poimirlem26  37847  cdleme32d  40704  cdleme32f  40706  cdlemksv2  41107  cdlemkuv2  41127  hlhilset  42194  aomclem8  43303  binomcxplemdvsum  44596  refsum2cn  45283  fmuldfeq  45829  fprodcnlem  45845  fprodcn  45846  fnlimfv  45907  fnlimcnv  45911  fnlimfvre  45918  fnlimfvre2  45921  fnlimf  45922  fnlimabslt  45923  fprodcncf  46144  dvnmptdivc  46182  dvmptfprod  46189  dvnprodlem1  46190  stoweidlem26  46270  stoweidlem31  46275  stoweidlem34  46278  stoweidlem35  46279  stoweidlem42  46286  stoweidlem48  46292  stoweidlem59  46303  fourierdlem31  46382  fourierdlem112  46462  sge0iunmptlemfi  46657  sge0iunmptlemre  46659  sge0iunmpt  46662  hoicvrrex  46800  ovncvrrp  46808  ovnhoilem1  46845  ovnlecvr2  46854  vonicc  46929  smflim  47021  smfmullem4  47038  smflim2  47050  smflimmpt  47054  smfsup  47058  smfsupmpt  47059  smfinf  47062  smfinfmpt  47063  smflimsuplem2  47065  smflimsuplem5  47068  smflimsup  47072  smflimsupmpt  47073  smfliminf  47075  smfliminfmpt  47076  fsupdm  47086  finfdm  47090  aacllem  50046