Theorem cbvmptv 4129

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-opab 4095  df-mpt 4096

This theorem is referenced by:  fnmptfvd  5666  frecsuc  6465  pw2f1odclem  6895  xpmapen  6911  omp1eom  7161  fodjuomni  7215  fodjumkv  7226  nninfwlporlemd  7238  nninfwlpor  7240  nninfwlpoim  7244  caucvgsrlembnd  7868  negiso  8982  infrenegsupex  9668  frec2uzsucd  10493  frecuzrdgdom  10510  frecuzrdgfun  10512  frecuzrdgsuct  10516  0tonninf  10532  1tonninf  10533  seq3f1oleml  10608  seq3f1o  10609  hashfz1  10875  xrnegiso  11427  infxrnegsupex  11428  climcvg1n  11515  summodc  11548  zsumdc  11549  fsum3  11552  fsumadd  11571  prodmodc  11743  zproddc  11744  fprodseq  11748  phimullem  12393  eulerthlemh  12399  eulerthlemth  12400  ennnfonelemnn0  12639  ennnfonelemr  12640  ctinfom  12645  grplactcnv  13234  expcn  14805  cdivcncfap  14840  expcncf  14845  ivthdich  14889  plyadd  14987  plymul  14988  plyco  14995  plycjlemc  14996  plycj  14997  dvply2g  15002  lgseisenlem3  15313  2sqlem1  15355  bj-charfunbi  15457  subctctexmid  15645  nninfsellemqall  15659  nninfomni  15663  nninffeq  15664  exmidsbthrlem  15666  exmidsbthr  15667  isomninn  15675  iswomninn  15694  ismkvnn  15697