Theorem nfmpt 5249

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Ⅎwnfc 2890  {copab 5205   ↦ cmpt 5225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-opab 5206  df-mpt 5226

This theorem is referenced by:  ovmpt3rab1  7691  nfof  7703  mpocurryvald  8295  nfrdg  8454  mapxpen  9183  nfoi  9554  seqof2  14101  nfsum1  15726  nfsum  15727  fsumrlim  15847  fsumo1  15848  nfcprod1  15944  nfcprod  15945  gsum2d2  19992  prdsgsum  19999  dprd2d2  20064  gsumdixp  20316  mpfrcl  22109  ptbasfi  23589  ptcnplem  23629  ptcnp  23630  cnmptk2  23694  cnmpt2k  23696  xkocnv  23822  fsumcn  24894  itg2cnlem1  25796  nfitg  25810  itgfsum  25862  dvmptfsum  26013  itgulm2  26452  lgamgulm2  27079  nosupbnd2  27761  noinfbnd2  27776  fmptcof2  32667  fpwrelmap  32744  nfesum2  34042  sigapildsys  34163  oms0  34299  bnj1366  34843  exrecfnlem  37380  poimirlem26  37653  cdleme32d  40446  cdleme32f  40448  cdlemksv2  40849  cdlemkuv2  40869  hlhilset  41936  pwsgprod  42554  aomclem8  43073  binomcxplemdvsum  44374  refsum2cn  45043  fmuldfeq  45598  fprodcnlem  45614  fprodcn  45615  fnlimfv  45678  fnlimcnv  45682  fnlimfvre  45689  fnlimfvre2  45692  fnlimf  45693  fnlimabslt  45694  fprodcncf  45915  dvnmptdivc  45953  dvmptfprod  45960  dvnprodlem1  45961  stoweidlem26  46041  stoweidlem31  46046  stoweidlem34  46049  stoweidlem35  46050  stoweidlem42  46057  stoweidlem48  46063  stoweidlem59  46074  fourierdlem31  46153  fourierdlem112  46233  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  sge0iunmpt  46433  hoicvrrex  46571  ovncvrrp  46579  ovnhoilem1  46616  ovnlecvr2  46625  vonicc  46700  smflim  46792  smfmullem4  46809  smflim2  46821  smflimmpt  46825  smfsup  46829  smfsupmpt  46830  smfinf  46833  smfinfmpt  46834  smflimsuplem2  46836  smflimsuplem5  46839  smflimsup  46843  smflimsupmpt  46844  smfliminf  46846  smfliminfmpt  46847  fsupdm  46857  finfdm  46861  aacllem  49320