Theorem cbvmptv 4222

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

Syntax hints:   -> wi 4   = wceq 1402   |-> cmpt 4187

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-opab 4188  df-mpt 4189

This theorem is referenced by:  fnmptfvd  5804  frecsuc  6668  pw2f1odclem  7124  xpmapen  7140  omp1eom  7425  fodjuomni  7479  fodjumkv  7490  nninfwlporlemd  7502  nninfwlpor  7504  nninfwlpoim  7509  nninfinfwlpo  7510  caucvgsrlembnd  8158  negiso  9275  infrenegsupex  9973  frec2uzsucd  10816  frecuzrdgdom  10833  frecuzrdgfun  10835  frecuzrdgsuct  10839  0tonninf  10855  1tonninf  10856  seq3f1oleml  10931  seq3f1o  10932  hashfz1  11200  xrnegiso  12006  infxrnegsupex  12007  climcvg1n  12094  summodc  12128  zsumdc  12129  fsum3  12132  fsumadd  12151  prodmodc  12323  zproddc  12324  fprodseq  12328  phimullem  12981  eulerthlemh  12987  eulerthlemth  12988  ballotfilemfval  13207  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemi  13221  ballotfilemsval  13230  ballotfilemsv  13231  ballotfilemsf1o  13235  ballotfilemrval  13239  ballotfilemrinv  13255  ballotfi  13260  ennnfonelemnn0  13291  ennnfonelemr  13292  ctinfom  13297  grplactcnv  13884  expcn  15593  cdivcncfap  15628  expcncf  15633  ivthdich  15677  plyadd  15775  plymul  15776  plyco  15783  plycjlemc  15784  plycj  15785  dvply2g  15790  lgseisenlem3  16105  2sqlem1  16147  bj-charfunbi  16751  subctctexmid  16944  nninfsellemqall  16963  nninfomni  16967  nninffeq  16968  exmidsbthrlem  16972  exmidsbthr  16973  isomninn  16985  iswomninn  17005  ismkvnn  17008