Theorem nfmpt 5209

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 5193	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2918	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2943	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1934	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 5180	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2924	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2147  Ⅎwnfc 2911  {copab 5173   ↦ cmpt 5192

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-opab 5174  df-mpt 5193

This theorem is used by:  ovmpt3rab1  7711  nfof  7731  mpocurryvald  8325  nfrdg  8460  mapxpen  9200  nfoi  9545  seqof2  14243  nfsum1  15901  nfsum  15902  fsumrlim  16022  fsumo1  16023  nfcprod1  16121  nfcprod  16122  gsum2d2  20239  prdsgsum  20246  dprd2d2  20311  gsumdixp  20599  pwsgprod  20610  mpfrcl  22449  ptbasfi  23955  ptcnplem  23995  ptcnp  23996  cnmptk2  24060  cnmpt2k  24062  xkocnv  24188  fsumcn  25246  itg2cnlem1  26137  nfitg  26150  itgfsum  26202  dvmptfsum  26350  itgulm2  26793  lgamgulm2  27420  nosupbnd2  28130  noinfbnd2  28145  fmptcof2  33349  fpwrelmap  33421  nfesum2  34784  sigapildsys  34906  oms0  35040  bnj1366  35570  exrecfnlem  38570  poimirlem26  38832  cdleme32d  41767  cdleme32f  41769  cdlemksv2  42170  cdlemkuv2  42190  hlhilset  43257  aomclem8  44329  binomcxplemdvsum  45600  refsum2cn  46329  fmuldfeq  46868  fprodcnlem  46884  fprodcn  46885  fnlimfv  46946  fnlimcnv  46950  fnlimfvre  46957  fnlimfvre2  46960  fnlimf  46961  fnlimabslt  46962  fprodcncf  47183  dvnmptdivc  47221  dvmptfprod  47228  dvnprodlem1  47229  stoweidlem26  47309  stoweidlem31  47314  stoweidlem34  47317  stoweidlem35  47318  stoweidlem42  47325  stoweidlem48  47331  stoweidlem59  47342  fourierdlem31  47421  fourierdlem112  47501  sge0iunmptlemfi  47696  sge0iunmptlemre  47698  sge0iunmpt  47701  hoicvrrex  47839  ovncvrrp  47847  ovnhoilem1  47884  ovnlecvr2  47893  vonicc  47968  smflim  48060  smfmullem4  48077  smflim2  48089  smflimmpt  48093  smfsup  48097  smfsupmpt  48098  smfinf  48101  smfinfmpt  48102  smflimsuplem2  48104  smflimsuplem5  48107  smflimsup  48111  smflimsupmpt  48112  smfliminf  48114  smfliminfmpt  48115  fsupdm  48125  finfdm  48129  aacllem  51367