Theorem cbvmpov 7249

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 5167, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)

Hypotheses

Ref	Expression
cbvmpov.1	⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)
cbvmpov.2	⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷)

Assertion

Ref	Expression
cbvmpov	⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)

Distinct variable groups:   𝑥,𝑤,𝑦,𝑧,𝐴   𝑤,𝐵,𝑥,𝑦,𝑧   𝑤,𝐶,𝑧   𝑥,𝐷,𝑦

Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐷(𝑧,𝑤)   𝐸(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem cbvmpov

Step	Hyp	Ref	Expression
1		nfcv 2977	. 2 ⊢ Ⅎ𝑧𝐶
2		nfcv 2977	. 2 ⊢ Ⅎ𝑤𝐶
3		nfcv 2977	. 2 ⊢ Ⅎ𝑥𝐷
4		nfcv 2977	. 2 ⊢ Ⅎ𝑦𝐷
5		cbvmpov.1	. . 3 ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)
6		cbvmpov.2	. . 3 ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷)
7	5, 6	sylan9eq 2876	. 2 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)
8	1, 2, 3, 4, 7	cbvmpo 7248	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)

Syntax hints:   → wi 4   = wceq 1537   ∈ cmpo 7158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5129  df-oprab 7160  df-mpo 7161

This theorem is referenced by:  fvproj  7828  seqomlem0  8085  dffi3  8895  cantnfsuc  9133  fin23lem33  9767  om2uzrdg  13325  uzrdgsuci  13329  sadcp1  15804  smupp1  15829  imasvscafn  16810  mgmnsgrpex  18096  sgrpnmndex  18097  sylow1  18728  sylow2b  18748  sylow3lem5  18756  sylow3  18758  efgmval  18838  efgtf  18848  frlmphl  20925  pmatcollpw3lem  21391  mp2pm2mplem3  21416  txbas  22175  bcth  23932  opnmbl  24203  mbfimaopn  24257  mbfi1fseq  24322  motplusg  26328  ttgval  26661  opsqrlem3  29919  fedgmul  31027  mdetpmtr12  31090  madjusmdetlem4  31095  dya2iocival  31531  sxbrsigalem5  31546  sxbrsigalem6  31547  eulerpart  31640  sseqp1  31653  cvmliftlem15  32545  cvmlift2  32563  opnmbllem0  34943  mblfinlem1  34944  mblfinlem2  34945  sdc  35034  tendoplcbv  37926  dvhvaddcbv  38240  dvhvscacbv  38249  fsovcnvlem  40408  ntrneibex  40472  ioorrnopn  42639  hoidmvle  42931  ovnhoi  42934  hoimbl  42962  smflimlem6  43101  funcrngcsetc  44318  funcrngcsetcALT  44319  funcringcsetc  44355  lmod1zr  44597