Theorem cbvmptv 4180

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 4179	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

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

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 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-opab 4146  df-mpt 4147

This theorem is referenced by:  fnmptfvd  5744  frecsuc  6564  pw2f1odclem  7008  xpmapen  7024  omp1eom  7278  fodjuomni  7332  fodjumkv  7343  nninfwlporlemd  7355  nninfwlpor  7357  nninfwlpoim  7362  nninfinfwlpo  7363  caucvgsrlembnd  8004  negiso  9118  infrenegsupex  9806  frec2uzsucd  10640  frecuzrdgdom  10657  frecuzrdgfun  10659  frecuzrdgsuct  10663  0tonninf  10679  1tonninf  10680  seq3f1oleml  10755  seq3f1o  10756  hashfz1  11022  xrnegiso  11794  infxrnegsupex  11795  climcvg1n  11882  summodc  11915  zsumdc  11916  fsum3  11919  fsumadd  11938  prodmodc  12110  zproddc  12111  fprodseq  12115  phimullem  12768  eulerthlemh  12774  eulerthlemth  12775  ennnfonelemnn0  13014  ennnfonelemr  13015  ctinfom  13020  grplactcnv  13656  expcn  15264  cdivcncfap  15299  expcncf  15304  ivthdich  15348  plyadd  15446  plymul  15447  plyco  15454  plycjlemc  15455  plycj  15456  dvply2g  15461  lgseisenlem3  15772  2sqlem1  15814  bj-charfunbi  16283  subctctexmid  16479  nninfsellemqall  16495  nninfomni  16499  nninffeq  16500  exmidsbthrlem  16504  exmidsbthr  16505  isomninn  16513  iswomninn  16532  ismkvnn  16535