Theorem cbvmptv 4126

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-opab 4092  df-mpt 4093

This theorem is referenced by:  fnmptfvd  5663  frecsuc  6462  pw2f1odclem  6892  xpmapen  6908  omp1eom  7156  fodjuomni  7210  fodjumkv  7221  nninfwlporlemd  7233  nninfwlpor  7235  nninfwlpoim  7239  caucvgsrlembnd  7863  negiso  8976  infrenegsupex  9662  frec2uzsucd  10475  frecuzrdgdom  10492  frecuzrdgfun  10494  frecuzrdgsuct  10498  0tonninf  10514  1tonninf  10515  seq3f1oleml  10590  seq3f1o  10591  hashfz1  10857  xrnegiso  11408  infxrnegsupex  11409  climcvg1n  11496  summodc  11529  zsumdc  11530  fsum3  11533  fsumadd  11552  prodmodc  11724  zproddc  11725  fprodseq  11729  phimullem  12366  eulerthlemh  12372  eulerthlemth  12373  ennnfonelemnn0  12582  ennnfonelemr  12583  ctinfom  12588  grplactcnv  13177  expcn  14748  cdivcncfap  14783  expcncf  14788  ivthdich  14832  plyadd  14930  plymul  14931  plyco  14937  plycjlemc  14938  plycj  14939  lgseisenlem3  15229  2sqlem1  15271  bj-charfunbi  15373  subctctexmid  15561  nninfsellemqall  15575  nninfomni  15579  nninffeq  15580  exmidsbthrlem  15582  exmidsbthr  15583  isomninn  15591  iswomninn  15610  ismkvnn  15613