Theorem nfmpt 5202

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 5186	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2914	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2939	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1931	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 5173	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2920	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569   ∈ wcel 2144  Ⅎwnfc 2907  {copab 5166   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-opab 5167  df-mpt 5186

This theorem is used by:  ovmpt3rab1  7680  nfof  7700  mpocurryvald  8291  nfrdg  8426  mapxpen  9166  nfoi  9512  seqof2  14207  nfsum1  15863  nfsum  15864  fsumrlim  15984  fsumo1  15985  nfcprod1  16083  nfcprod  16084  gsum2d2  20194  prdsgsum  20201  dprd2d2  20266  gsumdixp  20554  pwsgprod  20565  mpfrcl  22400  ptbasfi  23906  ptcnplem  23946  ptcnp  23947  cnmptk2  24011  cnmpt2k  24013  xkocnv  24139  fsumcn  25197  itg2cnlem1  26088  nfitg  26101  itgfsum  26153  dvmptfsum  26301  itgulm2  26742  lgamgulm2  27369  nosupbnd2  28079  noinfbnd2  28094  fmptcof2  33299  fpwrelmap  33372  nfesum2  34720  sigapildsys  34842  oms0  34976  bnj1366  35506  exrecfnlem  38396  poimirlem26  38658  cdleme32d  41595  cdleme32f  41597  cdlemksv2  41998  cdlemkuv2  42018  hlhilset  43085  aomclem8  44157  binomcxplemdvsum  45433  refsum2cn  46149  fmuldfeq  46689  fprodcnlem  46705  fprodcn  46706  fnlimfv  46767  fnlimcnv  46771  fnlimfvre  46778  fnlimfvre2  46781  fnlimf  46782  fnlimabslt  46783  fprodcncf  47004  dvnmptdivc  47042  dvmptfprod  47049  dvnprodlem1  47050  stoweidlem26  47130  stoweidlem31  47135  stoweidlem34  47138  stoweidlem35  47139  stoweidlem42  47146  stoweidlem48  47152  stoweidlem59  47163  fourierdlem31  47242  fourierdlem112  47322  sge0iunmptlemfi  47517  sge0iunmptlemre  47519  sge0iunmpt  47522  hoicvrrex  47660  ovncvrrp  47668  ovnhoilem1  47705  ovnlecvr2  47714  vonicc  47789  smflim  47881  smfmullem4  47898  smflim2  47910  smflimmpt  47914  smfsup  47918  smfsupmpt  47919  smfinf  47922  smfinfmpt  47923  smflimsuplem2  47925  smflimsuplem5  47928  smflimsup  47932  smflimsupmpt  47933  smfliminf  47935  smfliminfmpt  47936  fsupdm  47946  finfdm  47950  aacllem  51108