Theorem nfmpt 5256

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 5233	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2891	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2921	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1903	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 5218	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2902	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Ⅎwnfc 2884  {copab 5211   ↦ cmpt 5232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-opab 5212  df-mpt 5233

This theorem is referenced by:  ovmpt3rab1  7664  nfof  7676  mpocurryvald  8255  nfrdg  8414  mapxpen  9143  nfoi  9509  seqof2  14026  nfsum1  15636  nfsum  15637  fsumrlim  15757  fsumo1  15758  nfcprod1  15854  nfcprod  15855  gsum2d2  19842  prdsgsum  19849  dprd2d2  19914  gsumdixp  20131  mpfrcl  21648  ptbasfi  23085  ptcnplem  23125  ptcnp  23126  cnmptk2  23190  cnmpt2k  23192  xkocnv  23318  fsumcn  24386  itg2cnlem1  25279  nfitg  25292  itgfsum  25344  dvmptfsum  25492  itgulm2  25921  lgamgulm2  26540  nosupbnd2  27219  noinfbnd2  27234  fmptcof2  31882  fpwrelmap  31958  nfesum2  33039  sigapildsys  33160  oms0  33296  bnj1366  33840  exrecfnlem  36260  poimirlem26  36514  cdleme32d  39315  cdleme32f  39317  cdlemksv2  39718  cdlemkuv2  39738  hlhilset  40805  pwsgprod  41114  aomclem8  41803  binomcxplemdvsum  43114  refsum2cn  43722  fmuldfeq  44299  fprodcnlem  44315  fprodcn  44316  fnlimfv  44379  fnlimcnv  44383  fnlimfvre  44390  fnlimfvre2  44393  fnlimf  44394  fnlimabslt  44395  fprodcncf  44616  dvnmptdivc  44654  dvmptfprod  44661  dvnprodlem1  44662  stoweidlem26  44742  stoweidlem31  44747  stoweidlem34  44750  stoweidlem35  44751  stoweidlem42  44758  stoweidlem48  44764  stoweidlem59  44775  fourierdlem31  44854  fourierdlem112  44934  sge0iunmptlemfi  45129  sge0iunmptlemre  45131  sge0iunmpt  45134  hoicvrrex  45272  ovncvrrp  45280  ovnhoilem1  45317  ovnlecvr2  45326  vonicc  45401  smflim  45493  smfmullem4  45510  smflim2  45522  smflimmpt  45526  smfsup  45530  smfsupmpt  45531  smfinf  45534  smfinfmpt  45535  smflimsuplem2  45537  smflimsuplem5  45540  smflimsup  45544  smflimsupmpt  45545  smfliminf  45547  smfliminfmpt  45548  fsupdm  45558  finfdm  45562  aacllem  47848