Theorem nfmpt 5195

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 5179	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2915	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2940	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1918	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 5166	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2921	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 399   = wceq 1559   ∈ wcel 2141  Ⅎwnfc 2908  {copab 5159   ↦ cmpt 5178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-opab 5160  df-mpt 5179

This theorem is referenced by:  ovmpt3rab1  7649  nfof  7661  mpocurryvald  8244  nfrdg  8379  mapxpen  9109  nfoi  9456  seqof2  14067  nfsum1  15708  nfsum  15709  fsumrlim  15830  fsumo1  15831  nfcprod1  15929  nfcprod  15930  gsum2d2  20005  prdsgsum  20012  dprd2d2  20077  gsumdixp  20354  pwsgprod  20365  mpfrcl  22126  ptbasfi  23629  ptcnplem  23669  ptcnp  23670  cnmptk2  23734  cnmpt2k  23736  xkocnv  23862  fsumcn  24920  itg2cnlem1  25811  nfitg  25825  itgfsum  25877  dvmptfsum  26025  itgulm2  26460  lgamgulm2  27088  nosupbnd2  27768  noinfbnd2  27783  fmptcof2  32820  fpwrelmap  32896  nfesum2  34299  sigapildsys  34420  oms0  34555  bnj1366  35085  exrecfnlem  37834  poimirlem26  38106  cdleme32d  41029  cdleme32f  41031  cdlemksv2  41432  cdlemkuv2  41452  hlhilset  42519  aomclem8  43599  binomcxplemdvsum  44892  refsum2cn  45579  fmuldfeq  46120  fprodcnlem  46136  fprodcn  46137  fnlimfv  46198  fnlimcnv  46202  fnlimfvre  46209  fnlimfvre2  46212  fnlimf  46213  fnlimabslt  46214  fprodcncf  46435  dvnmptdivc  46473  dvmptfprod  46480  dvnprodlem1  46481  stoweidlem26  46561  stoweidlem31  46566  stoweidlem34  46569  stoweidlem35  46570  stoweidlem42  46577  stoweidlem48  46583  stoweidlem59  46594  fourierdlem31  46673  fourierdlem112  46753  sge0iunmptlemfi  46948  sge0iunmptlemre  46950  sge0iunmpt  46953  hoicvrrex  47091  ovncvrrp  47099  ovnhoilem1  47136  ovnlecvr2  47145  vonicc  47220  smflim  47312  smfmullem4  47329  smflim2  47341  smflimmpt  47345  smfsup  47349  smfsupmpt  47350  smfinf  47353  smfinfmpt  47354  smflimsuplem2  47356  smflimsuplem5  47359  smflimsup  47363  smflimsupmpt  47364  smfliminf  47366  smfliminfmpt  47367  fsupdm  47377  finfdm  47381  aacllem  50383