Theorem cbvmptv 4206

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

Syntax hints:   -> wi 4   = wceq 1398   |-> cmpt 4171

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-opab 4172  df-mpt 4173

This theorem is referenced by:  fnmptfvd  5782  frecsuc  6638  pw2f1odclem  7087  xpmapen  7103  omp1eom  7386  fodjuomni  7440  fodjumkv  7451  nninfwlporlemd  7463  nninfwlpor  7465  nninfwlpoim  7470  nninfinfwlpo  7471  caucvgsrlembnd  8116  negiso  9229  infrenegsupex  9926  frec2uzsucd  10763  frecuzrdgdom  10780  frecuzrdgfun  10782  frecuzrdgsuct  10786  0tonninf  10802  1tonninf  10803  seq3f1oleml  10878  seq3f1o  10879  hashfz1  11146  xrnegiso  11947  infxrnegsupex  11948  climcvg1n  12035  summodc  12069  zsumdc  12070  fsum3  12073  fsumadd  12092  prodmodc  12264  zproddc  12265  fprodseq  12269  phimullem  12922  eulerthlemh  12928  eulerthlemth  12929  ennnfonelemnn0  13173  ennnfonelemr  13174  ctinfom  13179  grplactcnv  13815  expcn  15434  cdivcncfap  15469  expcncf  15474  ivthdich  15518  plyadd  15616  plymul  15617  plyco  15624  plycjlemc  15625  plycj  15626  dvply2g  15631  lgseisenlem3  15945  2sqlem1  15987  bj-charfunbi  16581  subctctexmid  16774  nninfsellemqall  16793  nninfomni  16797  nninffeq  16798  exmidsbthrlem  16802  exmidsbthr  16803  isomninn  16815  iswomninn  16835  ismkvnn  16838