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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2111  Ⅎwnfc 2879  {copab 5148   ↦ cmpt 5167

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-opab 5149  df-mpt 5168

This theorem is referenced by:  ovmpt3rab1  7599  nfof  7611  mpocurryvald  8195  nfrdg  8328  mapxpen  9051  nfoi  9395  seqof2  13962  nfsum1  15592  nfsum  15593  fsumrlim  15713  fsumo1  15714  nfcprod1  15810  nfcprod  15811  gsum2d2  19881  prdsgsum  19888  dprd2d2  19953  gsumdixp  20232  mpfrcl  22015  ptbasfi  23491  ptcnplem  23531  ptcnp  23532  cnmptk2  23596  cnmpt2k  23598  xkocnv  23724  fsumcn  24783  itg2cnlem1  25684  nfitg  25698  itgfsum  25750  dvmptfsum  25901  itgulm2  26340  lgamgulm2  26968  nosupbnd2  27650  noinfbnd2  27665  fmptcof2  32631  fpwrelmap  32708  nfesum2  34046  sigapildsys  34167  oms0  34302  bnj1366  34833  exrecfnlem  37413  poimirlem26  37686  cdleme32d  40483  cdleme32f  40485  cdlemksv2  40886  cdlemkuv2  40906  hlhilset  41973  pwsgprod  42577  aomclem8  43094  binomcxplemdvsum  44388  refsum2cn  45075  fmuldfeq  45623  fprodcnlem  45639  fprodcn  45640  fnlimfv  45701  fnlimcnv  45705  fnlimfvre  45712  fnlimfvre2  45715  fnlimf  45716  fnlimabslt  45717  fprodcncf  45938  dvnmptdivc  45976  dvmptfprod  45983  dvnprodlem1  45984  stoweidlem26  46064  stoweidlem31  46069  stoweidlem34  46072  stoweidlem35  46073  stoweidlem42  46080  stoweidlem48  46086  stoweidlem59  46097  fourierdlem31  46176  fourierdlem112  46256  sge0iunmptlemfi  46451  sge0iunmptlemre  46453  sge0iunmpt  46456  hoicvrrex  46594  ovncvrrp  46602  ovnhoilem1  46639  ovnlecvr2  46648  vonicc  46723  smflim  46815  smfmullem4  46832  smflim2  46844  smflimmpt  46848  smfsup  46852  smfsupmpt  46853  smfinf  46856  smfinfmpt  46857  smflimsuplem2  46859  smflimsuplem5  46862  smflimsup  46866  smflimsupmpt  46867  smfliminf  46869  smfliminfmpt  46870  fsupdm  46880  finfdm  46884  aacllem  49833