Theorem nfmpt 5184

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Ⅎwnfc 2884  {copab 5148   ↦ cmpt 5167

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-opab 5149  df-mpt 5168

This theorem is referenced by:  ovmpt3rab1  7618  nfof  7630  mpocurryvald  8213  nfrdg  8346  mapxpen  9074  nfoi  9422  seqof2  14013  nfsum1  15643  nfsum  15644  fsumrlim  15765  fsumo1  15766  nfcprod1  15864  nfcprod  15865  gsum2d2  19940  prdsgsum  19947  dprd2d2  20012  gsumdixp  20289  pwsgprod  20300  mpfrcl  22073  ptbasfi  23556  ptcnplem  23596  ptcnp  23597  cnmptk2  23661  cnmpt2k  23663  xkocnv  23789  fsumcn  24847  itg2cnlem1  25738  nfitg  25752  itgfsum  25804  dvmptfsum  25952  itgulm2  26387  lgamgulm2  27013  nosupbnd2  27694  noinfbnd2  27709  fmptcof2  32745  fpwrelmap  32821  nfesum2  34201  sigapildsys  34322  oms0  34457  bnj1366  34987  exrecfnlem  37709  poimirlem26  37981  cdleme32d  40904  cdleme32f  40906  cdlemksv2  41307  cdlemkuv2  41327  hlhilset  42394  aomclem8  43507  binomcxplemdvsum  44800  refsum2cn  45487  fmuldfeq  46031  fprodcnlem  46047  fprodcn  46048  fnlimfv  46109  fnlimcnv  46113  fnlimfvre  46120  fnlimfvre2  46123  fnlimf  46124  fnlimabslt  46125  fprodcncf  46346  dvnmptdivc  46384  dvmptfprod  46391  dvnprodlem1  46392  stoweidlem26  46472  stoweidlem31  46477  stoweidlem34  46480  stoweidlem35  46481  stoweidlem42  46488  stoweidlem48  46494  stoweidlem59  46505  fourierdlem31  46584  fourierdlem112  46664  sge0iunmptlemfi  46859  sge0iunmptlemre  46861  sge0iunmpt  46864  hoicvrrex  47002  ovncvrrp  47010  ovnhoilem1  47047  ovnlecvr2  47056  vonicc  47131  smflim  47223  smfmullem4  47240  smflim2  47252  smflimmpt  47256  smfsup  47260  smfsupmpt  47261  smfinf  47264  smfinfmpt  47265  smflimsuplem2  47267  smflimsuplem5  47270  smflimsup  47274  smflimsupmpt  47275  smfliminf  47277  smfliminfmpt  47278  fsupdm  47288  finfdm  47292  aacllem  50288