Theorem nfmpt 5210

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 5194	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2923	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2948	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1926	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 5181	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2929	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 400   = wceq 1567   ∈ wcel 2149  Ⅎwnfc 2916  {copab 5174   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-opab 5175  df-mpt 5194

This theorem is referenced by:  ovmpt3rab1  7666  nfof  7678  mpocurryvald  8262  nfrdg  8397  mapxpen  9127  nfoi  9472  seqof2  14092  nfsum1  15737  nfsum  15738  fsumrlim  15859  fsumo1  15860  nfcprod1  15958  nfcprod  15959  gsum2d2  20040  prdsgsum  20047  dprd2d2  20112  gsumdixp  20396  pwsgprod  20407  mpfrcl  22201  ptbasfi  23703  ptcnplem  23743  ptcnp  23744  cnmptk2  23808  cnmpt2k  23810  xkocnv  23936  fsumcn  24994  itg2cnlem1  25885  nfitg  25899  itgfsum  25951  dvmptfsum  26099  itgulm2  26534  lgamgulm2  27162  nosupbnd2  27842  noinfbnd2  27857  fmptcof2  32939  fpwrelmap  33015  nfesum2  34372  sigapildsys  34493  oms0  34628  bnj1366  35158  exrecfnlem  37908  poimirlem26  38180  cdleme32d  41103  cdleme32f  41105  cdlemksv2  41506  cdlemkuv2  41526  hlhilset  42593  aomclem8  43673  binomcxplemdvsum  44950  refsum2cn  45643  fmuldfeq  46184  fprodcnlem  46200  fprodcn  46201  fnlimfv  46262  fnlimcnv  46266  fnlimfvre  46273  fnlimfvre2  46276  fnlimf  46277  fnlimabslt  46278  fprodcncf  46499  dvnmptdivc  46537  dvmptfprod  46544  dvnprodlem1  46545  stoweidlem26  46625  stoweidlem31  46630  stoweidlem34  46633  stoweidlem35  46634  stoweidlem42  46641  stoweidlem48  46647  stoweidlem59  46658  fourierdlem31  46737  fourierdlem112  46817  sge0iunmptlemfi  47012  sge0iunmptlemre  47014  sge0iunmpt  47017  hoicvrrex  47155  ovncvrrp  47163  ovnhoilem1  47200  ovnlecvr2  47209  vonicc  47284  smflim  47376  smfmullem4  47393  smflim2  47405  smflimmpt  47409  smfsup  47413  smfsupmpt  47414  smfinf  47417  smfinfmpt  47418  smflimsuplem2  47420  smflimsuplem5  47423  smflimsup  47427  smflimsupmpt  47428  smfliminf  47430  smfliminfmpt  47431  fsupdm  47441  finfdm  47445  aacllem  50457