Theorem nfmpt 4940

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 4924	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2942	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2964	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1990	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 4912	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2946	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 384   = wceq 1637   ∈ wcel 2156  Ⅎwnfc 2935  {copab 4906   ↦ cmpt 4923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-opab 4907  df-mpt 4924

This theorem is referenced by:  ovmpt3rab1  7117  nfof  7128  mpt2curryvald  7627  nfrdg  7742  mapxpen  8361  nfoi  8654  seqof2  13078  nfsum1  14639  nfsum  14640  fsumrlim  14761  fsumo1  14762  nfcprod1  14857  nfcprod  14858  gsum2d2  18570  prdsgsum  18574  dprd2d2  18641  gsumdixp  18807  mpfrcl  19722  ptbasfi  21595  ptcnplem  21635  ptcnp  21636  cnmptk2  21700  cnmpt2k  21702  xkocnv  21828  fsumcn  22883  itg2cnlem1  23741  nfitg  23754  itgfsum  23806  dvmptfsum  23951  itgulm2  24376  lgamgulm2  24975  fmptcof2  29783  fpwrelmap  29834  nfesum2  30427  sigapildsys  30549  oms0  30683  bnj1366  31221  nosupbnd2  32181  poimirlem26  33746  cdleme32d  36222  cdleme32f  36224  cdlemksv2  36625  cdlemkuv2  36645  hlhilset  37712  aomclem8  38129  binomcxplemdvsum  39051  refsum2cn  39688  wessf1ornlem  39857  fmuldfeq  40292  fprodcnlem  40308  fprodcn  40309  fnlimfv  40372  fnlimcnv  40376  fnlimfvre  40383  fnlimfvre2  40386  fnlimf  40387  fnlimabslt  40388  fprodcncf  40591  dvnmptdivc  40630  dvmptfprod  40637  dvnprodlem1  40638  stoweidlem26  40719  stoweidlem31  40724  stoweidlem34  40727  stoweidlem35  40728  stoweidlem42  40735  stoweidlem48  40741  stoweidlem59  40752  fourierdlem31  40831  fourierdlem112  40911  sge0iunmptlemfi  41106  sge0iunmptlemre  41108  sge0iunmpt  41111  hoicvrrex  41249  ovncvrrp  41257  ovnhoilem1  41294  ovnlecvr2  41303  vonicc  41378  smflim  41464  smfmullem4  41480  smflim2  41491  smflimmpt  41495  smfsup  41499  smfsupmpt  41500  smfinf  41503  smfinfmpt  41504  smflimsuplem2  41506  smflimsuplem5  41509  smflimsup  41513  smflimsupmpt  41514  smfliminf  41516  smfliminfmpt  41517  aacllem  43115