Theorem cbvmptv 4024

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

Syntax hints:   -> wi 4   = wceq 1331   |-> cmpt 3989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-opab 3990  df-mpt 3991

This theorem is referenced by:  frecsuc  6304  xpmapen  6744  omp1eom  6980  fodjuomni  7021  fodjumkv  7034  caucvgsrlembnd  7609  negiso  8713  infrenegsupex  9389  frec2uzsucd  10174  frecuzrdgdom  10191  frecuzrdgfun  10193  frecuzrdgsuct  10197  0tonninf  10212  1tonninf  10213  seq3f1oleml  10276  seq3f1o  10277  hashfz1  10529  xrnegiso  11031  infxrnegsupex  11032  climcvg1n  11119  summodc  11152  zsumdc  11153  fsum3  11156  fsumadd  11175  prodmodc  11347  phimullem  11901  ennnfonelemnn0  11935  ennnfonelemr  11936  ctinfom  11941  cdivcncfap  12756  expcncf  12761  subctctexmid  13196  nninfsellemqall  13211  nninfomni  13215  nninffeq  13216  exmidsbthrlem  13217  exmidsbthr  13218  isomninn  13226