Theorem cbvmpov 7361

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 5189, 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 2908	. 2 ⊢ Ⅎ𝑧𝐶
2		nfcv 2908	. 2 ⊢ Ⅎ𝑤𝐶
3		nfcv 2908	. 2 ⊢ Ⅎ𝑥𝐷
4		nfcv 2908	. 2 ⊢ Ⅎ𝑦𝐷
5		cbvmpov.1	. . 3 ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)
6		cbvmpov.2	. . 3 ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷)
7	5, 6	sylan9eq 2799	. 2 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)
8	1, 2, 3, 4, 7	cbvmpo 7360	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)

Syntax hints:   → wi 4   = wceq 1541   ∈ cmpo 7270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-opab 5141  df-oprab 7272  df-mpo 7273

This theorem is referenced by:  fvproj  7959  seqomlem0  8264  dffi3  9151  cantnfsuc  9389  fin23lem33  10085  om2uzrdg  13657  uzrdgsuci  13661  sadcp1  16143  smupp1  16168  imasvscafn  17229  mgmnsgrpex  18551  sgrpnmndex  18552  sylow1  19189  sylow2b  19209  sylow3lem5  19217  sylow3  19219  efgmval  19299  efgtf  19309  frlmphl  20969  pmatcollpw3lem  21913  mp2pm2mplem3  21938  txbas  22699  bcth  24474  opnmbl  24747  mbfimaopn  24801  mbfi1fseq  24867  motplusg  26884  ttgval  27217  ttgvalOLD  27218  opsqrlem3  30483  fedgmul  31691  mdetpmtr12  31754  madjusmdetlem4  31759  dya2iocival  32219  sxbrsigalem5  32234  sxbrsigalem6  32235  eulerpart  32328  sseqp1  32341  cvmliftlem15  33239  cvmlift2  33257  opnmbllem0  35792  mblfinlem1  35793  mblfinlem2  35794  sdc  35881  tendoplcbv  38768  dvhvaddcbv  39082  dvhvscacbv  39091  fsovcnvlem  41574  ntrneibex  41636  ioorrnopn  43800  hoidmvle  44092  ovnhoi  44095  hoimbl  44123  smflimlem6  44262  funcrngcsetc  45508  funcrngcsetcALT  45509  funcringcsetc  45545  lmod1zr  45786  functhinclem4  46277