Theorem cbvmptv 4156

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

Syntax hints:   -> wi 4   = wceq 1373   |-> cmpt 4121

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-opab 4122  df-mpt 4123

This theorem is referenced by:  fnmptfvd  5707  frecsuc  6516  pw2f1odclem  6956  xpmapen  6972  omp1eom  7223  fodjuomni  7277  fodjumkv  7288  nninfwlporlemd  7300  nninfwlpor  7302  nninfwlpoim  7307  nninfinfwlpo  7308  caucvgsrlembnd  7949  negiso  9063  infrenegsupex  9750  frec2uzsucd  10583  frecuzrdgdom  10600  frecuzrdgfun  10602  frecuzrdgsuct  10606  0tonninf  10622  1tonninf  10623  seq3f1oleml  10698  seq3f1o  10699  hashfz1  10965  xrnegiso  11688  infxrnegsupex  11689  climcvg1n  11776  summodc  11809  zsumdc  11810  fsum3  11813  fsumadd  11832  prodmodc  12004  zproddc  12005  fprodseq  12009  phimullem  12662  eulerthlemh  12668  eulerthlemth  12669  ennnfonelemnn0  12908  ennnfonelemr  12909  ctinfom  12914  grplactcnv  13549  expcn  15156  cdivcncfap  15191  expcncf  15196  ivthdich  15240  plyadd  15338  plymul  15339  plyco  15346  plycjlemc  15347  plycj  15348  dvply2g  15353  lgseisenlem3  15664  2sqlem1  15706  bj-charfunbi  15946  subctctexmid  16139  nninfsellemqall  16154  nninfomni  16158  nninffeq  16159  exmidsbthrlem  16163  exmidsbthr  16164  isomninn  16172  iswomninn  16191  ismkvnn  16194