Theorem cbvmptv 4205

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

Syntax hints:   → wi 4   = wceq 1398   ↦ cmpt 4170

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-un 3214  df-sn 3694  df-pr 3695  df-op 3697  df-opab 4171  df-mpt 4172

This theorem is referenced by:  fnmptfvd  5781  frecsuc  6637  pw2f1odclem  7086  xpmapen  7102  omp1eom  7385  fodjuomni  7439  fodjumkv  7450  nninfwlporlemd  7462  nninfwlpor  7464  nninfwlpoim  7469  nninfinfwlpo  7470  caucvgsrlembnd  8115  negiso  9228  infrenegsupex  9925  frec2uzsucd  10762  frecuzrdgdom  10779  frecuzrdgfun  10781  frecuzrdgsuct  10785  0tonninf  10801  1tonninf  10802  seq3f1oleml  10877  seq3f1o  10878  hashfz1  11144  xrnegiso  11943  infxrnegsupex  11944  climcvg1n  12031  summodc  12065  zsumdc  12066  fsum3  12069  fsumadd  12088  prodmodc  12260  zproddc  12261  fprodseq  12265  phimullem  12918  eulerthlemh  12924  eulerthlemth  12925  ennnfonelemnn0  13165  ennnfonelemr  13166  ctinfom  13171  grplactcnv  13807  expcn  15426  cdivcncfap  15461  expcncf  15466  ivthdich  15510  plyadd  15608  plymul  15609  plyco  15616  plycjlemc  15617  plycj  15618  dvply2g  15623  lgseisenlem3  15937  2sqlem1  15979  bj-charfunbi  16573  subctctexmid  16766  nninfsellemqall  16785  nninfomni  16789  nninffeq  16790  exmidsbthrlem  16794  exmidsbthr  16795  isomninn  16807  iswomninn  16827  ismkvnn  16830