Theorem cbvmpov 7112

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

Syntax hints:   → wi 4   = wceq 1525   ∈ cmpo 7025

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-opab 5031  df-oprab 7027  df-mpo 7028

This theorem is referenced by:  seqomlem0  7943  dffi3  8748  cantnfsuc  8986  fin23lem33  9620  om2uzrdg  13178  uzrdgsuci  13182  sadcp1  15641  smupp1  15666  imasvscafn  16643  mgmnsgrpex  17861  sgrpnmndex  17862  sylow1  18462  sylow2b  18482  sylow3lem5  18490  sylow3  18492  efgmval  18569  efgtf  18579  frlmphl  20611  pmatcollpw3lem  21079  mp2pm2mplem3  21104  txbas  21863  bcth  23619  opnmbl  23890  mbfimaopn  23944  mbfi1fseq  24009  motplusg  26014  ttgval  26348  opsqrlem3  29606  fedgmul  30627  mdetpmtr12  30701  madjusmdetlem4  30706  fvproj  30709  dya2iocival  31144  sxbrsigalem5  31159  sxbrsigalem6  31160  eulerpart  31253  sseqp1  31266  cvmliftlem15  32155  cvmlift2  32173  opnmbllem0  34480  mblfinlem1  34481  mblfinlem2  34482  sdc  34572  tendoplcbv  37463  dvhvaddcbv  37777  dvhvscacbv  37786  fsovcnvlem  39865  ntrneibex  39929  ioorrnopn  42154  hoidmvle  42446  ovnhoi  42449  hoimbl  42477  smflimlem6  42616  funcrngcsetc  43769  funcrngcsetcALT  43770  funcringcsetc  43806  lmod1zr  44050