Theorem cbvmpt 4971

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 2015	. . . 4 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)
2		nfv 2015	. . . . 5 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴
3		nfs1v 2313	. . . . 5 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝑧 = 𝐵
4	2, 3	nfan 2004	. . . 4 ⊢ Ⅎ𝑥(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
5		eleq1w 2888	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
6		sbequ12 2288	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
7	5, 6	anbi12d 626	. . . 4 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
8	1, 4, 7	cbvopab1 4945	. . 3 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
9		nfv 2015	. . . . 5 ⊢ Ⅎ𝑦 𝑤 ∈ 𝐴
10		cbvmpt.1	. . . . . . 7 ⊢ Ⅎ𝑦𝐵
11	10	nfeq2 2984	. . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝐵
12	11	nfsb 2574	. . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝑧 = 𝐵
13	9, 12	nfan 2004	. . . 4 ⊢ Ⅎ𝑦(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
14		nfv 2015	. . . 4 ⊢ Ⅎ𝑤(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)
15		eleq1w 2888	. . . . 5 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
16		sbequ 2506	. . . . . 6 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵))
17		cbvmpt.2	. . . . . . . 8 ⊢ Ⅎ𝑥𝐶
18	17	nfeq2 2984	. . . . . . 7 ⊢ Ⅎ𝑥 𝑧 = 𝐶
19		cbvmpt.3	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
20	19	eqeq2d 2834	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
21	18, 20	sbie 2538	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶)
22	16, 21	syl6bb 279	. . . . 5 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
23	15, 22	anbi12d 626	. . . 4 ⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
24	13, 14, 23	cbvopab1 4945	. . 3 ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
25	8, 24	eqtri 2848	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
26		df-mpt 4952	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
27		df-mpt 4952	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
28	25, 26, 27	3eqtr4i 2858	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1658  [wsb 2069   ∈ wcel 2166  Ⅎwnfc 2955  {copab 4934   ↦ cmpt 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-rab 3125  df-v 3415  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-nul 4144  df-if 4306  df-sn 4397  df-pr 4399  df-op 4403  df-opab 4935  df-mpt 4952

This theorem is referenced by:  cbvmptv  4972  dffn5f  6498  fvmpts  6531  fvmpt2i  6536  fvmptex  6540  fmptcof  6646  fmptcos  6647  fliftfuns  6818  offval2  7173  ofmpteq  7175  mpt2curryvald  7660  qliftfuns  8098  axcc2  9573  ac6num  9615  seqof2  13152  summolem2a  14822  zsum  14825  fsumcvg2  14834  fsumrlim  14916  cbvprod  15017  prodmolem2a  15036  zprod  15039  fprod  15043  pcmptdvds  15968  prdsdsval2  16496  gsumconstf  18687  gsummpt1n0  18716  gsum2d2  18725  dprd2d2  18796  gsumdixp  18962  psrass1lem  19737  coe1fzgsumdlem  20030  gsumply1eq  20034  evl1gsumdlem  20079  madugsum  20816  cnmpt1t  21838  cnmpt2k  21861  elmptrab  22000  flfcnp2  22180  prdsxmet  22543  fsumcn  23042  ovoliunlem3  23669  ovoliun  23670  ovoliun2  23671  voliun  23719  mbfpos  23816  mbfposb  23818  i1fposd  23872  itg2cnlem1  23926  isibl2  23931  cbvitg  23940  itgss3  23979  itgfsum  23991  itgabs  23999  itgcn  24007  limcmpt  24045  dvmptfsum  24136  lhop2  24176  dvfsumle  24182  dvfsumlem2  24188  itgsubstlem  24209  itgsubst  24210  itgulm2  24561  rlimcnp2  25105  gsummpt2co  30324  esumsnf  30670  mbfposadd  33999  itgabsnc  34021  ftc1cnnclem  34025  ftc2nc  34036  mzpsubst  38154  rabdiophlem2  38209  aomclem8  38473  fsumcnf  39997  disjf1  40176  disjrnmpt2  40182  disjinfi  40187  fmptf  40248  cncfmptss  40613  mulc1cncfg  40615  expcnfg  40617  fprodcn  40626  fnlimabslt  40705  climmptf  40707  liminfvalxr  40809  icccncfext  40894  cncficcgt0  40895  cncfiooicclem1  40900  fprodcncf  40908  dvmptmulf  40946  iblsplitf  40979  stoweidlem21  41031  stirlinglem4  41087  stirlinglem13  41096  stirlinglem15  41098  fourierd  41232  fourierclimd  41233  sge0iunmptlemre  41422  sge0iunmpt  41425  sge0ltfirpmpt2  41433  sge0isummpt2  41439  sge0xaddlem2  41441  sge0xadd  41442  meadjiun  41473  meaiunincf  41490  meaiuninc3  41492  omeiunle  41524  caratheodorylem2  41534  ovncvrrp  41571  vonioo  41689  smflim2  41805  smfsup  41813  smfinf  41817  smflimsup  41827  smfliminf  41830