Theorem cbvmptv 4125

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

Syntax hints:   -> wi 4   = wceq 1364   |-> cmpt 4090

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-opab 4091  df-mpt 4092

This theorem is referenced by:  fnmptfvd  5662  frecsuc  6460  pw2f1odclem  6890  xpmapen  6906  omp1eom  7154  fodjuomni  7208  fodjumkv  7219  nninfwlporlemd  7231  nninfwlpor  7233  nninfwlpoim  7237  caucvgsrlembnd  7861  negiso  8974  infrenegsupex  9659  frec2uzsucd  10472  frecuzrdgdom  10489  frecuzrdgfun  10491  frecuzrdgsuct  10495  0tonninf  10511  1tonninf  10512  seq3f1oleml  10587  seq3f1o  10588  hashfz1  10854  xrnegiso  11405  infxrnegsupex  11406  climcvg1n  11493  summodc  11526  zsumdc  11527  fsum3  11530  fsumadd  11549  prodmodc  11721  zproddc  11722  fprodseq  11726  phimullem  12363  eulerthlemh  12369  eulerthlemth  12370  ennnfonelemnn0  12579  ennnfonelemr  12580  ctinfom  12585  grplactcnv  13174  cdivcncfap  14758  expcncf  14763  ivthdich  14807  plyadd  14897  plymul  14898  lgseisenlem3  15188  2sqlem1  15201  bj-charfunbi  15303  subctctexmid  15491  nninfsellemqall  15505  nninfomni  15509  nninffeq  15510  exmidsbthrlem  15512  exmidsbthr  15513  isomninn  15521  iswomninn  15540  ismkvnn  15543