Theorem cbvmptf 5179

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.) (Revised by Thierry Arnoux, 9-Mar-2017.) Add disjoint variable condition to avoid ax-13 2380. See cbvmptfg 5180 for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024.)

Hypotheses

Ref	Expression
cbvmptf.1	⊢ Ⅎ𝑥𝐴
cbvmptf.2	⊢ Ⅎ𝑦𝐴
cbvmptf.3	⊢ Ⅎ𝑦𝐵
cbvmptf.4	⊢ Ⅎ𝑥𝐶
cbvmptf.5	⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)

Assertion

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

Distinct variable group:   𝑥,𝑦

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

Proof of Theorem cbvmptf

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

Step	Hyp	Ref	Expression
1		nfv 1921	. . . 4 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)
2		cbvmptf.1	. . . . . 6 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2894	. . . . 5 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴
4		nfs1v 2167	. . . . 5 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝑧 = 𝐵
5	3, 4	nfan 1906	. . . 4 ⊢ Ⅎ𝑥(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
6		eleq1w 2823	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
7		sbequ12 2263	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
8	6, 7	anbi12d 638	. . . 4 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
9	1, 5, 8	cbvopab1 5153	. . 3 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
10		cbvmptf.2	. . . . . 6 ⊢ Ⅎ𝑦𝐴
11	10	nfcri 2894	. . . . 5 ⊢ Ⅎ𝑦 𝑤 ∈ 𝐴
12		cbvmptf.3	. . . . . . 7 ⊢ Ⅎ𝑦𝐵
13	12	nfeq2 2919	. . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝐵
14	13	nfsbv 2339	. . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝑧 = 𝐵
15	11, 14	nfan 1906	. . . 4 ⊢ Ⅎ𝑦(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
16		nfv 1921	. . . 4 ⊢ Ⅎ𝑤(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)
17		eleq1w 2823	. . . . 5 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
18		cbvmptf.4	. . . . . . 7 ⊢ Ⅎ𝑥𝐶
19	18	nfeq2 2919	. . . . . 6 ⊢ Ⅎ𝑥 𝑧 = 𝐶
20		cbvmptf.5	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
21	20	eqeq2d 2751	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
22	19, 21	sbhypf 3493	. . . . 5 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
23	17, 22	anbi12d 638	. . . 4 ⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
24	15, 16, 23	cbvopab1 5153	. . 3 ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
25	9, 24	eqtri 2763	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
26		df-mpt 5161	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
27		df-mpt 5161	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
28	25, 26, 27	3eqtr4i 2773	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547  [wsb 2073   ∈ wcel 2119  Ⅎwnfc 2887  {copab 5141   ↦ cmpt 5160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-opab 5142  df-mpt 5161

This theorem is referenced by:  cbvmpt  5181  resmptf  5998  fvmpt2f  6943  offval2f  7642  suppss2f  32737  fmptdF  32755  acunirnmpt2f  32760  funcnv4mpt  32767  cbvesum  34233  esumpfinvalf  34267  binomcxplemdvbinom  44804  binomcxplemdvsum  44806  binomcxplemnotnn0  44807  fmptff  45720  supxrleubrnmptf  45901  fnlimfv  46113  fnlimfvre2  46127  fnlimf  46128  limsupequzmptf  46181  sge0iunmptlemre  46865  smflim  47227  smflim2  47256  smfsup  47264  smfinf  47268  smflimsuplem2  47271  smflimsuplem5  47274  smflimsup  47278  smfliminf  47281