Theorem nfmpt 5127

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

Syntax hints:   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Ⅎwnfc 2936  {copab 5092   ↦ cmpt 5110

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-opab 5093  df-mpt 5111

This theorem is referenced by:  ovmpt3rab1  7383  nfof  7394  mpocurryvald  7919  nfrdg  8033  mapxpen  8667  nfoi  8962  seqof2  13424  nfsum1  15038  nfsum  15039  nfsumOLD  15040  fsumrlim  15158  fsumo1  15159  nfcprod1  15256  nfcprod  15257  gsum2d2  19087  prdsgsum  19094  dprd2d2  19159  gsumdixp  19355  mpfrcl  20757  ptbasfi  22186  ptcnplem  22226  ptcnp  22227  cnmptk2  22291  cnmpt2k  22293  xkocnv  22419  fsumcn  23475  itg2cnlem1  24365  nfitg  24378  itgfsum  24430  dvmptfsum  24578  itgulm2  25004  lgamgulm2  25621  fmptcof2  30420  fpwrelmap  30495  nfesum2  31410  sigapildsys  31531  oms0  31665  bnj1366  32211  nosupbnd2  33329  exrecfnlem  34796  poimirlem26  35083  cdleme32d  37740  cdleme32f  37742  cdlemksv2  38143  cdlemkuv2  38163  hlhilset  39230  aomclem8  40005  binomcxplemdvsum  41059  refsum2cn  41667  fmuldfeq  42225  fprodcnlem  42241  fprodcn  42242  fnlimfv  42305  fnlimcnv  42309  fnlimfvre  42316  fnlimfvre2  42319  fnlimf  42320  fnlimabslt  42321  fprodcncf  42542  dvnmptdivc  42580  dvmptfprod  42587  dvnprodlem1  42588  stoweidlem26  42668  stoweidlem31  42673  stoweidlem34  42676  stoweidlem35  42677  stoweidlem42  42684  stoweidlem48  42690  stoweidlem59  42701  fourierdlem31  42780  fourierdlem112  42860  sge0iunmptlemfi  43052  sge0iunmptlemre  43054  sge0iunmpt  43057  hoicvrrex  43195  ovncvrrp  43203  ovnhoilem1  43240  ovnlecvr2  43249  vonicc  43324  smflim  43410  smfmullem4  43426  smflim2  43437  smflimmpt  43441  smfsup  43445  smfsupmpt  43446  smfinf  43449  smfinfmpt  43450  smflimsuplem2  43452  smflimsuplem5  43455  smflimsup  43459  smflimsupmpt  43460  smfliminf  43462  smfliminfmpt  43463  aacllem  45329