Theorem cbvmptf 4883

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 Thierry Arnoux, 9-Mar-2017.)

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 1995	. . . 4 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)
2		cbvmptf.1	. . . . . 6 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2907	. . . . 5 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴
4		nfs1v 2274	. . . . 5 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝑧 = 𝐵
5	3, 4	nfan 1980	. . . 4 ⊢ Ⅎ𝑥(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
6		eleq1w 2833	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
7		sbequ12 2267	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
8	6, 7	anbi12d 616	. . . 4 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
9	1, 5, 8	cbvopab1 4858	. . 3 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
10		cbvmptf.2	. . . . . 6 ⊢ Ⅎ𝑦𝐴
11	10	nfcri 2907	. . . . 5 ⊢ Ⅎ𝑦 𝑤 ∈ 𝐴
12		cbvmptf.3	. . . . . . 7 ⊢ Ⅎ𝑦𝐵
13	12	nfeq2 2929	. . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝐵
14	13	nfsb 2590	. . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝑧 = 𝐵
15	11, 14	nfan 1980	. . . 4 ⊢ Ⅎ𝑦(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
16		nfv 1995	. . . 4 ⊢ Ⅎ𝑤(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)
17		eleq1w 2833	. . . . 5 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
18		cbvmptf.4	. . . . . . 7 ⊢ Ⅎ𝑥𝐶
19	18	nfeq2 2929	. . . . . 6 ⊢ Ⅎ𝑥 𝑧 = 𝐶
20		cbvmptf.5	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
21	20	eqeq2d 2781	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
22	19, 21	sbhypf 3405	. . . . 5 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
23	17, 22	anbi12d 616	. . . 4 ⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
24	15, 16, 23	cbvopab1 4858	. . 3 ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
25	9, 24	eqtri 2793	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
26		df-mpt 4865	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
27		df-mpt 4865	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
28	25, 26, 27	3eqtr4i 2803	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1631  [wsb 2049   ∈ wcel 2145  Ⅎwnfc 2900  {copab 4847   ↦ cmpt 4864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-opab 4848  df-mpt 4865

This theorem is referenced by:  resmptf  5591  fvmpt2f  6427  offval2f  7059  numclwwlk1lem2  27545  numclwwlk1lem2OLD  27546  suppss2f  29778  fmptdF  29795  acunirnmpt2f  29800  funcnv4mpt  29809  cbvesum  30443  esumpfinvalf  30477  binomcxplemdvbinom  39078  binomcxplemdvsum  39080  binomcxplemnotnn0  39081  supxrleubrnmptf  40193  fnlimfv  40410  fnlimfvre2  40424  fnlimf  40425  limsupequzmptf  40478  sge0iunmptlemre  41146  smflim  41502  smflim2  41529  smfsup  41537  smfinf  41541  smflimsuplem2  41544  smflimsuplem5  41547  smflimsup  41551  smfliminf  41554