Theorem cbvmpt 4499

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.)

Hypotheses

Ref	Expression
cbvmpt.1
cbvmpt.2
cbvmpt.3

Assertion

Ref	Expression
cbvmpt

Distinct variable groups:   ,   ,

Proof of Theorem cbvmpt

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1674	. . . 4
2		nfv 1674	. . . . 5
3		nfs1v 2151	. . . . 5
4	2, 3	nfan 1866	. . . 4
5		eleq1 2526	. . . . 5
6		sbequ12 1948	. . . . 5
7	5, 6	anbi12d 710	. . . 4
8	1, 4, 7	cbvopab1 4479	. . 3
9		nfv 1674	. . . . 5
10		cbvmpt.1	. . . . . . 7
11	10	nfeq2 2633	. . . . . 6
12	11	nfsb 2155	. . . . 5
13	9, 12	nfan 1866	. . . 4
14		nfv 1674	. . . 4
15		eleq1 2526	. . . . 5
16		sbequ 2077	. . . . . 6
17		cbvmpt.2	. . . . . . . 8
18	17	nfeq2 2633	. . . . . . 7
19		cbvmpt.3	. . . . . . . 8
20	19	eqeq2d 2468	. . . . . . 7
21	18, 20	sbie 2110	. . . . . 6
22	16, 21	syl6bb 261	. . . . 5
23	15, 22	anbi12d 710	. . . 4
24	13, 14, 23	cbvopab1 4479	. . 3
25	8, 24	eqtri 2483	. 2
26		df-mpt 4469	. 2
27		df-mpt 4469	. 2
28	25, 26, 27	3eqtr4i 2493	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1370  [wsb 1702  e.wcel 1758  F/_wnfc 2602  {copab 4466  e.cmpt 4467

This theorem is referenced by:  cbvmptv  4500  dffn5f  5869  fvmpts  5899  fvmpt2i  5903  fvmptex  5907  fmptcof  6000  fmptcos  6001  fliftfuns  6138  offval2  6469  ofmpteq  6471  mpt2curryvald  6923  qliftfuns  7321  axcc2  8743  ac6num  8785  seqof2  12021  summolem2a  13350  zsum  13353  fsumcvg2  13362  fsumrlim  13432  pcmptdvds  14114  prdsdsval2  14581  gsumconstf  16590  gsummpt1n0  16625  gsum2d2  16635  dprd2d2  16718  gsumdixpOLD  16876  gsumdixp  16877  psrass1lem  17623  coe1fzgsumdlem  17937  evl1gsumdlem  17983  madugsum  18717  cnmpt1t  19637  cnmpt2k  19660  elmptrab  19799  flfcnp2  19979  prdsxmet  20343  fsumcn  20845  ovoliunlem3  21386  ovoliun  21387  ovoliun2  21388  voliun  21435  mbfpos  21529  mbfposb  21531  i1fposd  21585  itg2cnlem1  21639  isibl2  21644  cbvitg  21653  itgss3  21692  itgfsum  21704  itgabs  21712  itgcn  21720  limcmpt  21758  dvmptfsum  21847  lhop2  21887  dvfsumle  21893  dvfsumlem2  21899  itgsubstlem  21920  itgsubst  21921  itgulm2  22274  rlimcnp2  22760  xrge0tmd  26833  cbvprod  27884  prodmolem2a  27903  zprod  27906  fprod  27910  mbfposadd  28899  itgabsnc  28921  ftc1cnnclem  28925  ftc2nc  28936  mzpsubst  29545  rabdiophlem2  29600  aomclem8  29874  fsumcnf  30203  cncfmptss  30366  mulc1cncfg  30368  expcnfg  30371  icccncfext  30455  cncficcgt0  30456  cncfiooicclem1  30461  dvsinax  30470  iblsplitf  30517  itgiccshift  30527  itgsbtaddcnst  30529  stoweidlem21  30550  stirlinglem4  30606  stirlinglem13  30615  stirlinglem15  30617  dirkerval  30620  dirkerval2  30623  dirkercncflem2  30633  dirkercncflem3  30634  dirkercncflem4  30635  dirkercncf  30636  fourierdlem81  30717  fourierdlem92  30728  fourierdlem93  30729  fourierdlem101  30737  fourierdlem103  30739  fourierdlem104  30740  fourierdlem111  30747  fourierd  30752  fourierclimd  30753  gsumply1eq  31693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2809  df-v 3083  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-opab 4468  df-mpt 4469