Theorem cbvmptf 5212

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 2404. See cbvmptfg 5213 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 1944	. . . 4 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)
2		cbvmptf.1	. . . . . 6 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2917	. . . . 5 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴
4		nfs1v 2191	. . . . 5 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝑧 = 𝐵
5	3, 4	nfan 1929	. . . 4 ⊢ Ⅎ𝑥(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
6		eleq1w 2846	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
7		sbequ12 2287	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
8	6, 7	anbi12d 643	. . . 4 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
9	1, 5, 8	cbvopab1 5186	. . 3 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
10		cbvmptf.2	. . . . . 6 ⊢ Ⅎ𝑦𝐴
11	10	nfcri 2917	. . . . 5 ⊢ Ⅎ𝑦 𝑤 ∈ 𝐴
12		cbvmptf.3	. . . . . . 7 ⊢ Ⅎ𝑦𝐵
13	12	nfeq2 2942	. . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝐵
14	13	nfsbv 2363	. . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝑧 = 𝐵
15	11, 14	nfan 1929	. . . 4 ⊢ Ⅎ𝑦(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
16		nfv 1944	. . . 4 ⊢ Ⅎ𝑤(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)
17		eleq1w 2846	. . . . 5 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
18		cbvmptf.4	. . . . . . 7 ⊢ Ⅎ𝑥𝐶
19	18	nfeq2 2942	. . . . . 6 ⊢ Ⅎ𝑥 𝑧 = 𝐶
20		cbvmptf.5	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
21	20	eqeq2d 2774	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
22	19, 21	sbhypf 3514	. . . . 5 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
23	17, 22	anbi12d 643	. . . 4 ⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
24	15, 16, 23	cbvopab1 5186	. . 3 ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
25	9, 24	eqtri 2786	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
26		df-mpt 5194	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
27		df-mpt 5194	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
28	25, 26, 27	3eqtr4i 2796	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570  [wsb 2096   ∈ wcel 2143  Ⅎwnfc 2910  {copab 5174   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-opab 5175  df-mpt 5194

This theorem is referenced by:  cbvmpt  5214  resmptf  6043  fvmpt2f  6992  offval2f  7691  suppss2f  32961  fmptdF  32979  acunirnmpt2f  32984  funcnv4mpt  32991  cbvesum  34410  esumpfinvalf  34444  binomcxplemdvbinom  45043  binomcxplemdvsum  45045  binomcxplemnotnn0  45046  fmptff  45964  supxrleubrnmptf  46145  fnlimfv  46357  fnlimfvre2  46371  fnlimf  46372  limsupequzmptf  46425  sge0iunmptlemre  47109  smflim  47471  smflim2  47500  smfsup  47508  smfinf  47512  smflimsuplem2  47515  smflimsuplem5  47518  smflimsup  47522  smfliminf  47525