Theorem nfmpt 5254

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

Syntax hints:   ∧ wa 395   = wceq 1536   ∈ wcel 2105  Ⅎwnfc 2887  {copab 5209   ↦ cmpt 5230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-opab 5210  df-mpt 5231

This theorem is referenced by:  ovmpt3rab1  7690  nfof  7702  mpocurryvald  8293  nfrdg  8452  mapxpen  9181  nfoi  9551  seqof2  14097  nfsum1  15722  nfsum  15723  fsumrlim  15843  fsumo1  15844  nfcprod1  15940  nfcprod  15941  gsum2d2  20006  prdsgsum  20013  dprd2d2  20078  gsumdixp  20332  mpfrcl  22126  ptbasfi  23604  ptcnplem  23644  ptcnp  23645  cnmptk2  23709  cnmpt2k  23711  xkocnv  23837  fsumcn  24907  itg2cnlem1  25810  nfitg  25824  itgfsum  25876  dvmptfsum  26027  itgulm2  26466  lgamgulm2  27093  nosupbnd2  27775  noinfbnd2  27790  fmptcof2  32673  fpwrelmap  32750  nfesum2  34021  sigapildsys  34142  oms0  34278  bnj1366  34821  exrecfnlem  37361  poimirlem26  37632  cdleme32d  40426  cdleme32f  40428  cdlemksv2  40829  cdlemkuv2  40849  hlhilset  41916  pwsgprod  42530  aomclem8  43049  binomcxplemdvsum  44350  refsum2cn  44975  fmuldfeq  45538  fprodcnlem  45554  fprodcn  45555  fnlimfv  45618  fnlimcnv  45622  fnlimfvre  45629  fnlimfvre2  45632  fnlimf  45633  fnlimabslt  45634  fprodcncf  45855  dvnmptdivc  45893  dvmptfprod  45900  dvnprodlem1  45901  stoweidlem26  45981  stoweidlem31  45986  stoweidlem34  45989  stoweidlem35  45990  stoweidlem42  45997  stoweidlem48  46003  stoweidlem59  46014  fourierdlem31  46093  fourierdlem112  46173  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  sge0iunmpt  46373  hoicvrrex  46511  ovncvrrp  46519  ovnhoilem1  46556  ovnlecvr2  46565  vonicc  46640  smflim  46732  smfmullem4  46749  smflim2  46761  smflimmpt  46765  smfsup  46769  smfsupmpt  46770  smfinf  46773  smfinfmpt  46774  smflimsuplem2  46776  smflimsuplem5  46779  smflimsup  46783  smflimsupmpt  46784  smfliminf  46786  smfliminfmpt  46787  fsupdm  46797  finfdm  46801  aacllem  49031