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  5741  frecsuc  6559  pw2f1odclem  7003  xpmapen  7019  omp1eom  7270  fodjuomni  7324  fodjumkv  7335  nninfwlporlemd  7347  nninfwlpor  7349  nninfwlpoim  7354  nninfinfwlpo  7355  caucvgsrlembnd  7996  negiso  9110  infrenegsupex  9797  frec2uzsucd  10631  frecuzrdgdom  10648  frecuzrdgfun  10650  frecuzrdgsuct  10654  0tonninf  10670  1tonninf  10671  seq3f1oleml  10746  seq3f1o  10747  hashfz1  11013  xrnegiso  11781  infxrnegsupex  11782  climcvg1n  11869  summodc  11902  zsumdc  11903  fsum3  11906  fsumadd  11925  prodmodc  12097  zproddc  12098  fprodseq  12102  phimullem  12755  eulerthlemh  12761  eulerthlemth  12762  ennnfonelemnn0  13001  ennnfonelemr  13002  ctinfom  13007  grplactcnv  13643  expcn  15251  cdivcncfap  15286  expcncf  15291  ivthdich  15335  plyadd  15433  plymul  15434  plyco  15441  plycjlemc  15442  plycj  15443  dvply2g  15448  lgseisenlem3  15759  2sqlem1  15801  bj-charfunbi  16198  subctctexmid  16395  nninfsellemqall  16411  nninfomni  16415  nninffeq  16416  exmidsbthrlem  16420  exmidsbthr  16421  isomninn  16429  iswomninn  16448  ismkvnn  16451