Theorem nfmpt 4540

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:   ,

Proof of Theorem nfmpt

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-mpt 4512	. 2
2		nfmpt.1	. . . . 5
3	2	nfcri 2612	. . . 4
4		nfmpt.2	. . . . 5
5	4	nfeq2 2636	. . . 4
6	3, 5	nfan 1928	. . 3
7	6	nfopab 4517	. 2
8	1, 7	nfcxfr 2617	1

Syntax hints:  /\wa 369  =wceq 1395  e.wcel 1818  F/_wnfc 2605  {copab 4509  e.cmpt 4510

This theorem is referenced by:  ovmpt3rab1  6534  mpt2curryvald  7018  nfrdg  7099  mapxpen  7703  nfoi  7960  seqof2  12165  nfsum1  13512  nfsum  13513  fsumrlim  13625  fsumo1  13626  nfcprod1  13717  nfcprod  13718  gsum2d2  17002  prdsgsum  17007  prdsgsumOLD  17008  dprd2d2  17093  gsumdixpOLD  17257  gsumdixp  17258  mpfrcl  18187  ptbasfi  20082  ptcnplem  20122  ptcnp  20123  cnmptk2  20187  cnmpt2k  20189  xkocnv  20315  fsumcn  21374  itg2cnlem1  22168  nfitg  22181  itgfsum  22233  dvmptfsum  22376  itgulm2  22804  fmptcof2  27502  fpwrelmap  27556  oms0  28266  lgamgulm2  28578  aomclem8  31007  binomcxplemdvsum  31260  refsum2cn  31413  fmuldfeq  31577  fprodcncf  31704  dvnmptdivc  31735  dvmptfprod  31742  dvnprodlem1  31743  stoweidlem26  31808  stoweidlem31  31813  stoweidlem34  31816  stoweidlem35  31817  stoweidlem42  31824  stoweidlem48  31830  stoweidlem59  31841  fourierdlem31  31920  fourierdlem112  32001  aacllem  33216  bnj1366  33888  cdleme32d  36170  cdleme32f  36172  cdlemksv2  36573  cdlemkuv2  36593  hlhilset  37664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-opab 4511  df-mpt 4512