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  9285  infrenegsupex  9994  frec2uzsucd  10838  frecuzrdgdom  10855  frecuzrdgfun  10857  frecuzrdgsuct  10861  0tonninf  10877  1tonninf  10878  seq3f1oleml  10953  seq3f1o  10954  hashfz1  11222  xrnegiso  12028  infxrnegsupex  12029  climcvg1n  12116  summodc  12150  zsumdc  12151  fsum3  12154  fsumadd  12173  prodmodc  12345  zproddc  12346  fprodseq  12350  phimullem  13003  eulerthlemh  13009  eulerthlemth  13010  ballotfilemfval  13229  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemi  13243  ballotfilemsval  13252  ballotfilemsv  13253  ballotfilemsf1o  13257  ballotfilemrval  13261  ballotfilemrinv  13277  ballotfi  13282  ennnfonelemnn0  13313  ennnfonelemr  13314  ctinfom  13319  grplactcnv  13907  expcn  15670  cdivcncfap  15705  expcncf  15710  ivthdich  15754  plyadd  15852  plymul  15853  plyco  15860  plycjlemc  15861  plycj  15862  dvply2g  15867  lgseisenlem3  16191  2sqlem1  16233  bj-charfunbi  16837  subctctexmid  17030  nninfsellemqall  17058  nninfomni  17062  nninffeq  17063  exmidsbthrlem  17067  exmidsbthr  17068  isomninn  17080  iswomninn  17100  ismkvnn  17103