Theorem nfmpt 5170

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

Syntax hints:   ∧ wa 396   = wceq 1547   ∈ wcel 2119  Ⅎwnfc 2886  {copab 5134   ↦ cmpt 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-opab 5135  df-mpt 5154

This theorem is referenced by:  ovmpt3rab1  7614  nfof  7626  mpocurryvald  8210  nfrdg  8343  mapxpen  9071  nfoi  9419  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  22061  ptbasfi  23564  ptcnplem  23604  ptcnp  23605  cnmptk2  23669  cnmpt2k  23671  xkocnv  23797  fsumcn  24855  itg2cnlem1  25746  nfitg  25760  itgfsum  25812  dvmptfsum  25960  itgulm2  26392  lgamgulm2  27017  nosupbnd2  27698  noinfbnd2  27713  fmptcof2  32749  fpwrelmap  32825  nfesum2  34225  sigapildsys  34346  oms0  34481  bnj1366  35011  exrecfnlem  37741  poimirlem26  38013  cdleme32d  40936  cdleme32f  40938  cdlemksv2  41339  cdlemkuv2  41359  hlhilset  42426  aomclem8  43506  binomcxplemdvsum  44799  refsum2cn  45486  fmuldfeq  46028  fprodcnlem  46044  fprodcn  46045  fnlimfv  46106  fnlimcnv  46110  fnlimfvre  46117  fnlimfvre2  46120  fnlimf  46121  fnlimabslt  46122  fprodcncf  46343  dvnmptdivc  46381  dvmptfprod  46388  dvnprodlem1  46389  stoweidlem26  46469  stoweidlem31  46474  stoweidlem34  46477  stoweidlem35  46478  stoweidlem42  46485  stoweidlem48  46491  stoweidlem59  46502  fourierdlem31  46581  fourierdlem112  46661  sge0iunmptlemfi  46856  sge0iunmptlemre  46858  sge0iunmpt  46861  hoicvrrex  46999  ovncvrrp  47007  ovnhoilem1  47044  ovnlecvr2  47053  vonicc  47128  smflim  47220  smfmullem4  47237  smflim2  47249  smflimmpt  47253  smfsup  47257  smfsupmpt  47258  smfinf  47261  smfinfmpt  47262  smflimsuplem2  47264  smflimsuplem5  47267  smflimsup  47271  smflimsupmpt  47272  smfliminf  47274  smfliminfmpt  47275  fsupdm  47285  finfdm  47289  aacllem  50291