Theorem nfmpt 5273

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 5250	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2900	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2926	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1898	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 5235	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2906	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 395   = wceq 1537   ∈ wcel 2108  Ⅎwnfc 2893  {copab 5228   ↦ cmpt 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-opab 5229  df-mpt 5250

This theorem is referenced by:  ovmpt3rab1  7708  nfof  7720  mpocurryvald  8311  nfrdg  8470  mapxpen  9209  nfoi  9583  seqof2  14111  nfsum1  15738  nfsum  15739  fsumrlim  15859  fsumo1  15860  nfcprod1  15956  nfcprod  15957  gsum2d2  20016  prdsgsum  20023  dprd2d2  20088  gsumdixp  20342  mpfrcl  22132  ptbasfi  23610  ptcnplem  23650  ptcnp  23651  cnmptk2  23715  cnmpt2k  23717  xkocnv  23843  fsumcn  24913  itg2cnlem1  25816  nfitg  25830  itgfsum  25882  dvmptfsum  26033  itgulm2  26470  lgamgulm2  27097  nosupbnd2  27779  noinfbnd2  27794  fmptcof2  32675  fpwrelmap  32747  nfesum2  34005  sigapildsys  34126  oms0  34262  bnj1366  34805  exrecfnlem  37345  poimirlem26  37606  cdleme32d  40401  cdleme32f  40403  cdlemksv2  40804  cdlemkuv2  40824  hlhilset  41891  pwsgprod  42499  aomclem8  43018  binomcxplemdvsum  44324  refsum2cn  44938  fmuldfeq  45504  fprodcnlem  45520  fprodcn  45521  fnlimfv  45584  fnlimcnv  45588  fnlimfvre  45595  fnlimfvre2  45598  fnlimf  45599  fnlimabslt  45600  fprodcncf  45821  dvnmptdivc  45859  dvmptfprod  45866  dvnprodlem1  45867  stoweidlem26  45947  stoweidlem31  45952  stoweidlem34  45955  stoweidlem35  45956  stoweidlem42  45963  stoweidlem48  45969  stoweidlem59  45980  fourierdlem31  46059  fourierdlem112  46139  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0iunmpt  46339  hoicvrrex  46477  ovncvrrp  46485  ovnhoilem1  46522  ovnlecvr2  46531  vonicc  46606  smflim  46698  smfmullem4  46715  smflim2  46727  smflimmpt  46731  smfsup  46735  smfsupmpt  46736  smfinf  46739  smfinfmpt  46740  smflimsuplem2  46742  smflimsuplem5  46745  smflimsup  46749  smflimsupmpt  46750  smfliminf  46752  smfliminfmpt  46753  fsupdm  46763  finfdm  46767  aacllem  48895