Theorem nfmpt 4746

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 4730	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2758	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2780	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1828	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 4718	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2762	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 384   = wceq 1483   ∈ wcel 1990  Ⅎwnfc 2751  {copab 4712   ↦ cmpt 4729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-opab 4713  df-mpt 4730

This theorem is referenced by:  ovmpt3rab1  6891  mpt2curryvald  7396  nfrdg  7510  mapxpen  8126  nfoi  8419  seqof2  12859  nfsum1  14420  nfsum  14421  fsumrlim  14543  fsumo1  14544  nfcprod1  14640  nfcprod  14641  gsum2d2  18373  prdsgsum  18377  dprd2d2  18443  gsumdixp  18609  mpfrcl  19518  ptbasfi  21384  ptcnplem  21424  ptcnp  21425  cnmptk2  21489  cnmpt2k  21491  xkocnv  21617  fsumcn  22673  itg2cnlem1  23528  nfitg  23541  itgfsum  23593  dvmptfsum  23738  itgulm2  24163  lgamgulm2  24762  fmptcof2  29457  fpwrelmap  29508  nfesum2  30103  sigapildsys  30225  oms0  30359  bnj1366  30900  nosupbnd2  31862  poimirlem26  33435  cdleme32d  35732  cdleme32f  35734  cdlemksv2  36135  cdlemkuv2  36155  hlhilset  37226  aomclem8  37631  binomcxplemdvsum  38554  refsum2cn  39197  wessf1ornlem  39371  fmuldfeq  39815  fprodcnlem  39831  fprodcn  39832  fnlimfv  39895  fnlimcnv  39899  fnlimfvre  39906  fnlimfvre2  39909  fnlimf  39910  fnlimabslt  39911  fprodcncf  40114  dvnmptdivc  40153  dvmptfprod  40160  dvnprodlem1  40161  stoweidlem26  40243  stoweidlem31  40248  stoweidlem34  40251  stoweidlem35  40252  stoweidlem42  40259  stoweidlem48  40265  stoweidlem59  40276  fourierdlem31  40355  fourierdlem112  40435  sge0iunmptlemfi  40630  sge0iunmptlemre  40632  sge0iunmpt  40635  hoicvrrex  40770  ovncvrrp  40778  ovnhoilem1  40815  ovnlecvr2  40824  vonicc  40899  smflim  40985  smfmullem4  41001  smflim2  41012  smflimmpt  41016  smfsup  41020  smfsupmpt  41021  smfinf  41024  smfinfmpt  41025  smflimsuplem2  41027  smflimsuplem5  41030  smflimsup  41034  smflimsupmpt  41035  smfliminf  41037  smfliminfmpt  41038  aacllem  42547