Theorem cbvmptv 4183

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

Syntax hints:   → wi 4   = wceq 1395   ↦ cmpt 4148

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-opab 4149  df-mpt 4150

This theorem is referenced by:  fnmptfvd  5747  frecsuc  6568  pw2f1odclem  7015  xpmapen  7031  omp1eom  7288  fodjuomni  7342  fodjumkv  7353  nninfwlporlemd  7365  nninfwlpor  7367  nninfwlpoim  7372  nninfinfwlpo  7373  caucvgsrlembnd  8014  negiso  9128  infrenegsupex  9821  frec2uzsucd  10656  frecuzrdgdom  10673  frecuzrdgfun  10675  frecuzrdgsuct  10679  0tonninf  10695  1tonninf  10696  seq3f1oleml  10771  seq3f1o  10772  hashfz1  11038  xrnegiso  11816  infxrnegsupex  11817  climcvg1n  11904  summodc  11937  zsumdc  11938  fsum3  11941  fsumadd  11960  prodmodc  12132  zproddc  12133  fprodseq  12137  phimullem  12790  eulerthlemh  12796  eulerthlemth  12797  ennnfonelemnn0  13036  ennnfonelemr  13037  ctinfom  13042  grplactcnv  13678  expcn  15286  cdivcncfap  15321  expcncf  15326  ivthdich  15370  plyadd  15468  plymul  15469  plyco  15476  plycjlemc  15477  plycj  15478  dvply2g  15483  lgseisenlem3  15794  2sqlem1  15836  bj-charfunbi  16356  subctctexmid  16551  nninfsellemqall  16567  nninfomni  16571  nninffeq  16572  exmidsbthrlem  16576  exmidsbthr  16577  isomninn  16585  iswomninn  16604  ismkvnn  16607