Theorem nfmpt 5186

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 5163	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2896	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2926	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1906	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 5148	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2907	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 396   = wceq 1542   ∈ wcel 2110  Ⅎwnfc 2889  {copab 5141   ↦ cmpt 5162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-opab 5142  df-mpt 5163

This theorem is referenced by:  ovmpt3rab1  7521  nfof  7533  mpocurryvald  8077  nfrdg  8236  mapxpen  8912  nfoi  9251  seqof2  13779  nfsum1  15399  nfsum  15400  nfsumOLD  15401  fsumrlim  15521  fsumo1  15522  nfcprod1  15618  nfcprod  15619  gsum2d2  19573  prdsgsum  19580  dprd2d2  19645  gsumdixp  19846  mpfrcl  21293  ptbasfi  22730  ptcnplem  22770  ptcnp  22771  cnmptk2  22835  cnmpt2k  22837  xkocnv  22963  fsumcn  24031  itg2cnlem1  24924  nfitg  24937  itgfsum  24989  dvmptfsum  25137  itgulm2  25566  lgamgulm2  26183  fmptcof2  30990  fpwrelmap  31064  nfesum2  32005  sigapildsys  32126  oms0  32260  bnj1366  32805  nosupbnd2  33915  noinfbnd2  33930  exrecfnlem  35546  poimirlem26  35799  cdleme32d  38454  cdleme32f  38456  cdlemksv2  38857  cdlemkuv2  38877  hlhilset  39944  pwsgprod  40266  aomclem8  40883  binomcxplemdvsum  41943  refsum2cn  42551  fmuldfeq  43095  fprodcnlem  43111  fprodcn  43112  fnlimfv  43175  fnlimcnv  43179  fnlimfvre  43186  fnlimfvre2  43189  fnlimf  43190  fnlimabslt  43191  fprodcncf  43412  dvnmptdivc  43450  dvmptfprod  43457  dvnprodlem1  43458  stoweidlem26  43538  stoweidlem31  43543  stoweidlem34  43546  stoweidlem35  43547  stoweidlem42  43554  stoweidlem48  43560  stoweidlem59  43571  fourierdlem31  43650  fourierdlem112  43730  sge0iunmptlemfi  43922  sge0iunmptlemre  43924  sge0iunmpt  43927  hoicvrrex  44065  ovncvrrp  44073  ovnhoilem1  44110  ovnlecvr2  44119  vonicc  44194  smflim  44280  smfmullem4  44296  smflim2  44307  smflimmpt  44311  smfsup  44315  smfsupmpt  44316  smfinf  44319  smfinfmpt  44320  smflimsuplem2  44322  smflimsuplem5  44325  smflimsup  44329  smflimsupmpt  44330  smfliminf  44332  smfliminfmpt  44333  aacllem  46474