Theorem nfmpt 5198

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Ⅎwnfc 2884  {copab 5162   ↦ cmpt 5181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-opab 5163  df-mpt 5182

This theorem is referenced by:  ovmpt3rab1  7626  nfof  7638  mpocurryvald  8222  nfrdg  8355  mapxpen  9083  nfoi  9431  seqof2  13995  nfsum1  15625  nfsum  15626  fsumrlim  15746  fsumo1  15747  nfcprod1  15843  nfcprod  15844  gsum2d2  19915  prdsgsum  19922  dprd2d2  19987  gsumdixp  20266  pwsgprod  20277  mpfrcl  22052  ptbasfi  23537  ptcnplem  23577  ptcnp  23578  cnmptk2  23642  cnmpt2k  23644  xkocnv  23770  fsumcn  24829  itg2cnlem1  25730  nfitg  25744  itgfsum  25796  dvmptfsum  25947  itgulm2  26386  lgamgulm2  27014  nosupbnd2  27696  noinfbnd2  27711  fmptcof2  32746  fpwrelmap  32822  nfesum2  34218  sigapildsys  34339  oms0  34474  bnj1366  35004  exrecfnlem  37631  poimirlem26  37894  cdleme32d  40817  cdleme32f  40819  cdlemksv2  41220  cdlemkuv2  41240  hlhilset  42307  aomclem8  43415  binomcxplemdvsum  44708  refsum2cn  45395  fmuldfeq  45940  fprodcnlem  45956  fprodcn  45957  fnlimfv  46018  fnlimcnv  46022  fnlimfvre  46029  fnlimfvre2  46032  fnlimf  46033  fnlimabslt  46034  fprodcncf  46255  dvnmptdivc  46293  dvmptfprod  46300  dvnprodlem1  46301  stoweidlem26  46381  stoweidlem31  46386  stoweidlem34  46389  stoweidlem35  46390  stoweidlem42  46397  stoweidlem48  46403  stoweidlem59  46414  fourierdlem31  46493  fourierdlem112  46573  sge0iunmptlemfi  46768  sge0iunmptlemre  46770  sge0iunmpt  46773  hoicvrrex  46911  ovncvrrp  46919  ovnhoilem1  46956  ovnlecvr2  46965  vonicc  47040  smflim  47132  smfmullem4  47149  smflim2  47161  smflimmpt  47165  smfsup  47169  smfsupmpt  47170  smfinf  47173  smfinfmpt  47174  smflimsuplem2  47176  smflimsuplem5  47179  smflimsup  47183  smflimsupmpt  47184  smfliminf  47186  smfliminfmpt  47187  fsupdm  47197  finfdm  47201  aacllem  50157