Theorem cbvmptv 4211

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	⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)

Assertion

Ref	Expression
cbvmptv	⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝑦,𝐵   𝑥,𝐶

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem cbvmptv

Step	Hyp	Ref	Expression
1		nfcv 2386	. 2 ⊢ Ⅎ𝑦𝐵
2		nfcv 2386	. 2 ⊢ Ⅎ𝑥𝐶
3		cbvmptv.1	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
4	1, 2, 3	cbvmpt 4210	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1398   ↦ cmpt 4176

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-opab 4177  df-mpt 4178

This theorem is referenced by:  fnmptfvd  5787  frecsuc  6651  pw2f1odclem  7100  xpmapen  7116  omp1eom  7399  fodjuomni  7453  fodjumkv  7464  nninfwlporlemd  7476  nninfwlpor  7478  nninfwlpoim  7483  nninfinfwlpo  7484  caucvgsrlembnd  8132  negiso  9246  infrenegsupex  9944  frec2uzsucd  10787  frecuzrdgdom  10804  frecuzrdgfun  10806  frecuzrdgsuct  10810  0tonninf  10826  1tonninf  10827  seq3f1oleml  10902  seq3f1o  10903  hashfz1  11171  xrnegiso  11972  infxrnegsupex  11973  climcvg1n  12060  summodc  12094  zsumdc  12095  fsum3  12098  fsumadd  12117  prodmodc  12289  zproddc  12290  fprodseq  12294  phimullem  12947  eulerthlemh  12953  eulerthlemth  12954  ballotfilemfval  13173  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemi  13187  ballotfilemsval  13196  ballotfilemsv  13197  ballotfilemsf1o  13201  ballotfilemrval  13205  ballotfilemrinv  13221  ballotfi  13226  ennnfonelemnn0  13257  ennnfonelemr  13258  ctinfom  13263  grplactcnv  13899  expcn  15546  cdivcncfap  15581  expcncf  15586  ivthdich  15630  plyadd  15728  plymul  15729  plyco  15736  plycjlemc  15737  plycj  15738  dvply2g  15743  lgseisenlem3  16057  2sqlem1  16099  bj-charfunbi  16693  subctctexmid  16886  nninfsellemqall  16905  nninfomni  16909  nninffeq  16910  exmidsbthrlem  16914  exmidsbthr  16915  isomninn  16927  iswomninn  16947  ismkvnn  16950