Theorem cbvmptf 5129

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 2379. See cbvmptfg 5130 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 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 1915	. . . 4 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)
2		cbvmptf.1	. . . . . 6 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2943	. . . . 5 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴
4		nfs1v 2157	. . . . 5 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝑧 = 𝐵
5	3, 4	nfan 1900	. . . 4 ⊢ Ⅎ𝑥(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
6		eleq1w 2872	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
7		sbequ12 2250	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
8	6, 7	anbi12d 633	. . . 4 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
9	1, 5, 8	cbvopab1 5103	. . 3 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
10		cbvmptf.2	. . . . . 6 ⊢ Ⅎ𝑦𝐴
11	10	nfcri 2943	. . . . 5 ⊢ Ⅎ𝑦 𝑤 ∈ 𝐴
12		cbvmptf.3	. . . . . . 7 ⊢ Ⅎ𝑦𝐵
13	12	nfeq2 2972	. . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝐵
14	13	nfsbv 2338	. . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝑧 = 𝐵
15	11, 14	nfan 1900	. . . 4 ⊢ Ⅎ𝑦(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
16		nfv 1915	. . . 4 ⊢ Ⅎ𝑤(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)
17		eleq1w 2872	. . . . 5 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
18		sbequ 2088	. . . . . 6 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵))
19		cbvmptf.4	. . . . . . . 8 ⊢ Ⅎ𝑥𝐶
20	19	nfeq2 2972	. . . . . . 7 ⊢ Ⅎ𝑥 𝑧 = 𝐶
21		cbvmptf.5	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
22	21	eqeq2d 2809	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
23	20, 22	sbiev 2322	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶)
24	18, 23	syl6bb 290	. . . . 5 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
25	17, 24	anbi12d 633	. . . 4 ⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
26	15, 16, 25	cbvopab1 5103	. . 3 ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
27	9, 26	eqtri 2821	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
28		df-mpt 5111	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
29		df-mpt 5111	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
30	27, 28, 29	3eqtr4i 2831	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  [wsb 2069   ∈ wcel 2111  Ⅎwnfc 2936  {copab 5092   ↦ cmpt 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5093  df-mpt 5111

This theorem is referenced by:  cbvmpt  5131  resmptf  5874  fvmpt2f  6746  offval2f  7401  suppss2f  30398  fmptdF  30419  acunirnmpt2f  30424  funcnv4mpt  30432  cbvesum  31411  esumpfinvalf  31445  binomcxplemdvbinom  41057  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  supxrleubrnmptf  42090  fnlimfv  42305  fnlimfvre2  42319  fnlimf  42320  limsupequzmptf  42373  sge0iunmptlemre  43054  smflim  43410  smflim2  43437  smfsup  43445  smfinf  43449  smflimsuplem2  43452  smflimsuplem5  43455  smflimsup  43459  smfliminf  43462