Theorem cbvmptv 4227

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 4226	1 |- ( x e. A |-> B ) = ( y e. A |-> C )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   |-> cmpt 4192

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-opab 4193  df-mpt 4194

This theorem is used by:  fnmptfvd  5813  frecsuc  6678  pw2f1odclem  7134  xpmapen  7150  omp1eom  7435  fodjuomni  7489  fodjumkv  7500  nninfwlporlemd  7512  nninfwlpor  7514  nninfwlpoim  7519  nninfinfwlpo  7520  caucvgsrlembnd  8168  negiso  9287  infrenegsupex  10003  frec2uzsucd  10851  frecuzrdgdom  10868  frecuzrdgfun  10870  frecuzrdgsuct  10874  0tonninf  10890  1tonninf  10891  seq3f1oleml  10966  seq3f1o  10967  hashfz1  11236  xrnegiso  12044  infxrnegsupex  12045  climcvg1n  12132  summodc  12166  zsumdc  12167  fsum3  12170  fsumadd  12189  prodmodc  12361  zproddc  12362  fprodseq  12366  phimullem  13023  eulerthlemh  13029  eulerthlemth  13030  ballotfilemfval  13278  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemi  13292  ballotfilemsval  13301  ballotfilemsv  13302  ballotfilemsf1o  13306  ballotfilemrval  13310  ballotfilemrinv  13326  ballotfi  13331  ennnfonelemnn0  13362  ennnfonelemr  13363  ctinfom  13368  grplactcnv  13956  expcn  15719  cdivcncfap  15754  expcncf  15759  ivthdich  15803  plyadd  15901  plymul  15902  plyco  15909  plycjlemc  15910  plycj  15911  dvply2g  15916  lgseisenlem3  16289  2sqlem1  16331  bj-charfunbi  16935  subctctexmid  17128  nninfsellemqall  17156  nninfomni  17160  nninffeq  17161  exmidsbthrlem  17165  exmidsbthr  17166  isomninn  17178  iswomninn  17198  ismkvnn  17201