Theorem cbvmptv 4229

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 2392	. 2 ⊢ Ⅎ𝑦𝐵
2		nfcv 2392	. 2 ⊢ Ⅎ𝑥𝐶
3		cbvmptv.1	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
4	1, 2, 3	cbvmpt 4228	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ↦ cmpt 4193

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 4194  df-mpt 4195

This theorem is used by:  fnmptfvd  5816  frecsuc  6682  pw2f1odclem  7139  xpmapen  7155  omp1eom  7442  fodjuomni  7496  fodjumkv  7507  nninfwlporlemd  7519  nninfwlpor  7521  nninfwlpoim  7526  nninfinfwlpo  7527  caucvgsrlembnd  8175  negiso  9294  infrenegsupex  10011  frec2uzsucd  10860  frecuzrdgdom  10877  frecuzrdgfun  10879  frecuzrdgsuct  10883  0tonninf  10899  1tonninf  10900  seq3f1oleml  10975  seq3f1o  10976  hashfz1  11245  xrnegiso  12054  infxrnegsupex  12055  climcvg1n  12142  summodc  12176  zsumdc  12177  fsum3  12180  fsumadd  12199  prodmodc  12371  zproddc  12372  fprodseq  12376  phimullem  13033  eulerthlemh  13039  eulerthlemth  13040  ballotfilemfval  13288  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemi  13302  ballotfilemsval  13311  ballotfilemsv  13312  ballotfilemsf1o  13316  ballotfilemrval  13320  ballotfilemrinv  13336  ballotfi  13341  ennnfonelemnn0  13372  ennnfonelemr  13373  ctinfom  13378  grplactcnv  13967  expcn  15807  cdivcncfap  15842  expcncf  15847  ivthdich  15891  plyadd  15989  plymul  15990  plyco  15997  plycjlemc  15998  plycj  15999  dvply2g  16004  lgseisenlem3  16408  2sqlem1  16450  bj-charfunbi  17054  subctctexmid  17247  nninfsellemqall  17276  nninfomni  17280  nninffeq  17281  exmidsbthrlem  17285  exmidsbthr  17286  isomninn  17298  iswomninn  17319  ismkvnn  17322