Theorem cbvmpt 4204

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.)

Hypotheses

Ref	Expression
cbvmpt.1	⊢ Ⅎ𝑦𝐵
cbvmpt.2	⊢ Ⅎ𝑥𝐶
cbvmpt.3	⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)

Assertion

Ref	Expression
cbvmpt	⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴

Allowed substitution hints:   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)

Proof of Theorem cbvmpt

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1577	. . . 4 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)
2		nfv 1577	. . . . 5 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴
3		nfs1v 1993	. . . . 5 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝑧 = 𝐵
4	2, 3	nfan 1614	. . . 4 ⊢ Ⅎ𝑥(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
5		eleq1 2295	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
6		sbequ12 1820	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
7	5, 6	anbi12d 473	. . . 4 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
8	1, 4, 7	cbvopab1 4182	. . 3 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
9		nfv 1577	. . . . 5 ⊢ Ⅎ𝑦 𝑤 ∈ 𝐴
10		cbvmpt.1	. . . . . . 7 ⊢ Ⅎ𝑦𝐵
11	10	nfeq2 2396	. . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝐵
12	11	nfsb 2000	. . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝑧 = 𝐵
13	9, 12	nfan 1614	. . . 4 ⊢ Ⅎ𝑦(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
14		nfv 1577	. . . 4 ⊢ Ⅎ𝑤(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)
15		eleq1 2295	. . . . 5 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
16		sbequ 1889	. . . . . 6 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵))
17		cbvmpt.2	. . . . . . . 8 ⊢ Ⅎ𝑥𝐶
18	17	nfeq2 2396	. . . . . . 7 ⊢ Ⅎ𝑥 𝑧 = 𝐶
19		cbvmpt.3	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
20	19	eqeq2d 2244	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
21	18, 20	sbie 1840	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶)
22	16, 21	bitrdi 196	. . . . 5 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
23	15, 22	anbi12d 473	. . . 4 ⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
24	13, 14, 23	cbvopab1 4182	. . 3 ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
25	8, 24	eqtri 2253	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
26		df-mpt 4172	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
27		df-mpt 4172	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
28	25, 26, 27	3eqtr4i 2263	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398  [wsb 1811   ∈ wcel 2203  Ⅎwnfc 2371  {copab 4169   ↦ 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:  cbvmptv  4205  dffn5imf  5731  fvmpts  5754  fvmpt2  5760  mptfvex  5762  fmptcof  5843  fmptcos  5844  fliftfuns  5970  offval2  6281  qliftfuns  6852  cc2  7577  summodclem2a  12060  zsumdc  12063  fsum3cvg2  12073  cbvprod  12237  zproddc  12258  fprodseq  12262  pcmptdvds  13036  gsumfzconstf  14048  cnmpt1t  15137  fsumcncntop  15419  limcmpted  15515  dvmptfsum  15577