Theorem nfmpt 5211

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2146  Ⅎwnfc 2912  {copab 5175   ↦ cmpt 5194

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-opab 5176  df-mpt 5195

This theorem is used by:  ovmpt3rab1  7674  nfof  7686  mpocurryvald  8268  nfrdg  8403  mapxpen  9134  nfoi  9479  seqof2  14109  nfsum1  15760  nfsum  15761  fsumrlim  15881  fsumo1  15882  nfcprod1  15980  nfcprod  15981  gsum2d2  20067  prdsgsum  20074  dprd2d2  20139  gsumdixp  20425  pwsgprod  20436  mpfrcl  22265  ptbasfi  23767  ptcnplem  23807  ptcnp  23808  cnmptk2  23872  cnmpt2k  23874  xkocnv  24000  fsumcn  25058  itg2cnlem1  25949  nfitg  25963  itgfsum  26015  dvmptfsum  26163  itgulm2  26601  lgamgulm2  27229  nosupbnd2  27909  noinfbnd2  27924  fmptcof2  33031  fpwrelmap  33107  nfesum2  34454  sigapildsys  34576  oms0  34711  bnj1366  35241  exrecfnlem  38058  poimirlem26  38330  cdleme32d  41251  cdleme32f  41253  cdlemksv2  41654  cdlemkuv2  41674  hlhilset  42741  aomclem8  43821  binomcxplemdvsum  45098  refsum2cn  45791  fmuldfeq  46332  fprodcnlem  46348  fprodcn  46349  fnlimfv  46410  fnlimcnv  46414  fnlimfvre  46421  fnlimfvre2  46424  fnlimf  46425  fnlimabslt  46426  fprodcncf  46647  dvnmptdivc  46685  dvmptfprod  46692  dvnprodlem1  46693  stoweidlem26  46773  stoweidlem31  46778  stoweidlem34  46781  stoweidlem35  46782  stoweidlem42  46789  stoweidlem48  46795  stoweidlem59  46806  fourierdlem31  46885  fourierdlem112  46965  sge0iunmptlemfi  47160  sge0iunmptlemre  47162  sge0iunmpt  47165  hoicvrrex  47303  ovncvrrp  47311  ovnhoilem1  47348  ovnlecvr2  47357  vonicc  47432  smflim  47524  smfmullem4  47541  smflim2  47553  smflimmpt  47557  smfsup  47561  smfsupmpt  47562  smfinf  47565  smfinfmpt  47566  smflimsuplem2  47568  smflimsuplem5  47571  smflimsup  47575  smflimsupmpt  47576  smfliminf  47578  smfliminfmpt  47579  fsupdm  47589  finfdm  47593  aacllem  50654