Theorem nfmpt 5203

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Ⅎwnfc 2907  {copab 5167   ↦ cmpt 5186

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-opab 5168  df-mpt 5187

This theorem is used by:  ovmpt3rab1  7673  nfof  7685  mpocurryvald  8269  nfrdg  8404  mapxpen  9144  nfoi  9489  seqof2  14127  nfsum1  15780  nfsum  15781  fsumrlim  15901  fsumo1  15902  nfcprod1  16000  nfcprod  16001  gsum2d2  20104  prdsgsum  20111  dprd2d2  20176  gsumdixp  20462  pwsgprod  20473  mpfrcl  22304  ptbasfi  23810  ptcnplem  23850  ptcnp  23851  cnmptk2  23915  cnmpt2k  23917  xkocnv  24043  fsumcn  25101  itg2cnlem1  25992  nfitg  26005  itgfsum  26057  dvmptfsum  26205  itgulm2  26648  lgamgulm2  27275  nosupbnd2  27955  noinfbnd2  27970  fmptcof2  33133  fpwrelmap  33207  nfesum2  34554  sigapildsys  34676  oms0  34811  bnj1366  35341  exrecfnlem  38136  poimirlem26  38398  cdleme32d  41320  cdleme32f  41322  cdlemksv2  41723  cdlemkuv2  41743  hlhilset  42810  aomclem8  43905  binomcxplemdvsum  45182  refsum2cn  45875  fmuldfeq  46416  fprodcnlem  46432  fprodcn  46433  fnlimfv  46494  fnlimcnv  46498  fnlimfvre  46505  fnlimfvre2  46508  fnlimf  46509  fnlimabslt  46510  fprodcncf  46731  dvnmptdivc  46769  dvmptfprod  46776  dvnprodlem1  46777  stoweidlem26  46857  stoweidlem31  46862  stoweidlem34  46865  stoweidlem35  46866  stoweidlem42  46873  stoweidlem48  46879  stoweidlem59  46890  fourierdlem31  46969  fourierdlem112  47049  sge0iunmptlemfi  47244  sge0iunmptlemre  47246  sge0iunmpt  47249  hoicvrrex  47387  ovncvrrp  47395  ovnhoilem1  47432  ovnlecvr2  47441  vonicc  47516  smflim  47608  smfmullem4  47625  smflim2  47637  smflimmpt  47641  smfsup  47645  smfsupmpt  47646  smfinf  47649  smfinfmpt  47650  smflimsuplem2  47652  smflimsuplem5  47655  smflimsup  47659  smflimsupmpt  47660  smfliminf  47662  smfliminfmpt  47663  fsupdm  47673  finfdm  47677  aacllem  50775