Theorem nfmpt 4896

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 4880	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2894	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2916	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1975	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 4868	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2898	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 383   = wceq 1630   ∈ wcel 2137  Ⅎwnfc 2887  {copab 4862   ↦ cmpt 4879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-opab 4863  df-mpt 4880

This theorem is referenced by:  ovmpt3rab1  7054  mpt2curryvald  7563  nfrdg  7677  mapxpen  8289  nfoi  8582  seqof2  13051  nfsum1  14617  nfsum  14618  fsumrlim  14740  fsumo1  14741  nfcprod1  14837  nfcprod  14838  gsum2d2  18571  prdsgsum  18575  dprd2d2  18641  gsumdixp  18807  mpfrcl  19718  ptbasfi  21584  ptcnplem  21624  ptcnp  21625  cnmptk2  21689  cnmpt2k  21691  xkocnv  21817  fsumcn  22872  itg2cnlem1  23725  nfitg  23738  itgfsum  23790  dvmptfsum  23935  itgulm2  24360  lgamgulm2  24959  fmptcof2  29764  fpwrelmap  29815  nfesum2  30410  sigapildsys  30532  oms0  30666  bnj1366  31205  nosupbnd2  32166  poimirlem26  33746  cdleme32d  36232  cdleme32f  36234  cdlemksv2  36635  cdlemkuv2  36655  hlhilset  37726  aomclem8  38131  binomcxplemdvsum  39054  refsum2cn  39694  wessf1ornlem  39868  fmuldfeq  40316  fprodcnlem  40332  fprodcn  40333  fnlimfv  40396  fnlimcnv  40400  fnlimfvre  40407  fnlimfvre2  40410  fnlimf  40411  fnlimabslt  40412  fprodcncf  40615  dvnmptdivc  40654  dvmptfprod  40661  dvnprodlem1  40662  stoweidlem26  40744  stoweidlem31  40749  stoweidlem34  40752  stoweidlem35  40753  stoweidlem42  40760  stoweidlem48  40766  stoweidlem59  40777  fourierdlem31  40856  fourierdlem112  40936  sge0iunmptlemfi  41131  sge0iunmptlemre  41133  sge0iunmpt  41136  hoicvrrex  41274  ovncvrrp  41282  ovnhoilem1  41319  ovnlecvr2  41328  vonicc  41403  smflim  41489  smfmullem4  41505  smflim2  41516  smflimmpt  41520  smfsup  41524  smfsupmpt  41525  smfinf  41528  smfinfmpt  41529  smflimsuplem2  41531  smflimsuplem5  41534  smflimsup  41538  smflimsupmpt  41539  smfliminf  41541  smfliminfmpt  41542  aacllem  43058