Theorem cbvmptv 4179

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

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

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 4145  df-mpt 4146

This theorem is referenced by:  fnmptfvd  5732  frecsuc  6543  pw2f1odclem  6983  xpmapen  6999  omp1eom  7250  fodjuomni  7304  fodjumkv  7315  nninfwlporlemd  7327  nninfwlpor  7329  nninfwlpoim  7334  nninfinfwlpo  7335  caucvgsrlembnd  7976  negiso  9090  infrenegsupex  9777  frec2uzsucd  10610  frecuzrdgdom  10627  frecuzrdgfun  10629  frecuzrdgsuct  10633  0tonninf  10649  1tonninf  10650  seq3f1oleml  10725  seq3f1o  10726  hashfz1  10992  xrnegiso  11759  infxrnegsupex  11760  climcvg1n  11847  summodc  11880  zsumdc  11881  fsum3  11884  fsumadd  11903  prodmodc  12075  zproddc  12076  fprodseq  12080  phimullem  12733  eulerthlemh  12739  eulerthlemth  12740  ennnfonelemnn0  12979  ennnfonelemr  12980  ctinfom  12985  grplactcnv  13621  expcn  15228  cdivcncfap  15263  expcncf  15268  ivthdich  15312  plyadd  15410  plymul  15411  plyco  15418  plycjlemc  15419  plycj  15420  dvply2g  15425  lgseisenlem3  15736  2sqlem1  15778  bj-charfunbi  16104  subctctexmid  16297  nninfsellemqall  16312  nninfomni  16316  nninffeq  16317  exmidsbthrlem  16321  exmidsbthr  16322  isomninn  16330  iswomninn  16349  ismkvnn  16352