Theorem cbvmptv 4183

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)

Hypothesis

Ref	Expression
cbvmptv.1	|- ( x = y -> B = C )

Assertion

Ref	Expression
cbvmptv	|- ( x e. A |-> B ) = ( y e. A |-> C )

Distinct variable groups:   x, A   y, A   y, B   x, C

Allowed substitution hints:   B( x)   C( y)

Proof of Theorem cbvmptv

Step	Hyp	Ref	Expression
1		nfcv 2372	. 2 |- F/_ y B
2		nfcv 2372	. 2 |- F/_ x C
3		cbvmptv.1	. 2 |- ( x = y -> B = C )
4	1, 2, 3	cbvmpt 4182	1 |- ( x e. A |-> B ) = ( y e. A |-> C )

Syntax hints:   -> wi 4   = wceq 1395   |-> cmpt 4148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-opab 4149  df-mpt 4150

This theorem is referenced by:  fnmptfvd  5747  frecsuc  6568  pw2f1odclem  7015  xpmapen  7031  omp1eom  7285  fodjuomni  7339  fodjumkv  7350  nninfwlporlemd  7362  nninfwlpor  7364  nninfwlpoim  7369  nninfinfwlpo  7370  caucvgsrlembnd  8011  negiso  9125  infrenegsupex  9818  frec2uzsucd  10653  frecuzrdgdom  10670  frecuzrdgfun  10672  frecuzrdgsuct  10676  0tonninf  10692  1tonninf  10693  seq3f1oleml  10768  seq3f1o  10769  hashfz1  11035  xrnegiso  11813  infxrnegsupex  11814  climcvg1n  11901  summodc  11934  zsumdc  11935  fsum3  11938  fsumadd  11957  prodmodc  12129  zproddc  12130  fprodseq  12134  phimullem  12787  eulerthlemh  12793  eulerthlemth  12794  ennnfonelemnn0  13033  ennnfonelemr  13034  ctinfom  13039  grplactcnv  13675  expcn  15283  cdivcncfap  15318  expcncf  15323  ivthdich  15367  plyadd  15465  plymul  15466  plyco  15473  plycjlemc  15474  plycj  15475  dvply2g  15480  lgseisenlem3  15791  2sqlem1  15833  bj-charfunbi  16342  subctctexmid  16537  nninfsellemqall  16553  nninfomni  16557  nninffeq  16558  exmidsbthrlem  16562  exmidsbthr  16563  isomninn  16571  iswomninn  16590  ismkvnn  16593