Theorem nfmpt 5256

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 5233	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2882	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2909	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1894	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 5218	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2889	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 394   = wceq 1533   ∈ wcel 2098  Ⅎwnfc 2875  {copab 5211   ↦ cmpt 5232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-opab 5212  df-mpt 5233

This theorem is referenced by:  ovmpt3rab1  7679  nfof  7691  mpocurryvald  8276  nfrdg  8435  mapxpen  9168  nfoi  9539  seqof2  14061  nfsum1  15672  nfsum  15673  fsumrlim  15793  fsumo1  15794  nfcprod1  15890  nfcprod  15891  gsum2d2  19941  prdsgsum  19948  dprd2d2  20013  gsumdixp  20267  mpfrcl  22053  ptbasfi  23529  ptcnplem  23569  ptcnp  23570  cnmptk2  23634  cnmpt2k  23636  xkocnv  23762  fsumcn  24832  itg2cnlem1  25735  nfitg  25748  itgfsum  25800  dvmptfsum  25951  itgulm2  26390  lgamgulm2  27013  nosupbnd2  27695  noinfbnd2  27710  fmptcof2  32524  fpwrelmap  32597  nfesum2  33788  sigapildsys  33909  oms0  34045  bnj1366  34588  exrecfnlem  36986  poimirlem26  37247  cdleme32d  40044  cdleme32f  40046  cdlemksv2  40447  cdlemkuv2  40467  hlhilset  41534  pwsgprod  41909  aomclem8  42624  binomcxplemdvsum  43931  refsum2cn  44539  fmuldfeq  45106  fprodcnlem  45122  fprodcn  45123  fnlimfv  45186  fnlimcnv  45190  fnlimfvre  45197  fnlimfvre2  45200  fnlimf  45201  fnlimabslt  45202  fprodcncf  45423  dvnmptdivc  45461  dvmptfprod  45468  dvnprodlem1  45469  stoweidlem26  45549  stoweidlem31  45554  stoweidlem34  45557  stoweidlem35  45558  stoweidlem42  45565  stoweidlem48  45571  stoweidlem59  45582  fourierdlem31  45661  fourierdlem112  45741  sge0iunmptlemfi  45936  sge0iunmptlemre  45938  sge0iunmpt  45941  hoicvrrex  46079  ovncvrrp  46087  ovnhoilem1  46124  ovnlecvr2  46133  vonicc  46208  smflim  46300  smfmullem4  46317  smflim2  46329  smflimmpt  46333  smfsup  46337  smfsupmpt  46338  smfinf  46341  smfinfmpt  46342  smflimsuplem2  46344  smflimsuplem5  46347  smflimsup  46351  smflimsupmpt  46352  smfliminf  46354  smfliminfmpt  46355  fsupdm  46365  finfdm  46369  aacllem  48417