Theorem cbvmptv 4100

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 2319	. 2 |- F/_ y B
2		nfcv 2319	. 2 |- F/_ x C
3		cbvmptv.1	. 2 |- ( x = y -> B = C )
4	1, 2, 3	cbvmpt 4099	1 |- ( x e. A |-> B ) = ( y e. A |-> C )

Syntax hints:   -> wi 4   = wceq 1353   |-> cmpt 4065

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-opab 4066  df-mpt 4067

This theorem is referenced by:  fnmptfvd  5621  frecsuc  6408  xpmapen  6850  omp1eom  7094  fodjuomni  7147  fodjumkv  7158  nninfwlporlemd  7170  nninfwlpor  7172  nninfwlpoim  7176  caucvgsrlembnd  7800  negiso  8912  infrenegsupex  9594  frec2uzsucd  10401  frecuzrdgdom  10418  frecuzrdgfun  10420  frecuzrdgsuct  10424  0tonninf  10439  1tonninf  10440  seq3f1oleml  10503  seq3f1o  10504  hashfz1  10763  xrnegiso  11270  infxrnegsupex  11271  climcvg1n  11358  summodc  11391  zsumdc  11392  fsum3  11395  fsumadd  11414  prodmodc  11586  zproddc  11587  fprodseq  11591  phimullem  12225  eulerthlemh  12231  eulerthlemth  12232  ennnfonelemnn0  12423  ennnfonelemr  12424  ctinfom  12429  grplactcnv  12972  cdivcncfap  14090  expcncf  14095  2sqlem1  14464  bj-charfunbi  14566  subctctexmid  14753  nninfsellemqall  14767  nninfomni  14771  nninffeq  14772  exmidsbthrlem  14773  exmidsbthr  14774  isomninn  14782  iswomninn  14801  ismkvnn  14804