Theorem cbvmpov 7457

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-opab 5173  df-oprab 7366  df-mpo 7367

This theorem is referenced by:  fvproj  8071  seqomlem0  8400  dffi3  9376  cantnfsuc  9615  fin23lem33  10290  om2uzrdg  13871  uzrdgsuci  13875  sadcp1  16346  smupp1  16371  imasvscafn  17433  mgmnsgrpex  18755  sgrpnmndex  18756  sylow1  19399  sylow2b  19419  sylow3lem5  19427  sylow3  19429  efgmval  19508  efgtf  19518  frlmphl  21224  pmatcollpw3lem  22169  mp2pm2mplem3  22194  txbas  22955  bcth  24730  opnmbl  25003  mbfimaopn  25057  mbfi1fseq  25123  motplusg  27547  ttgval  27880  ttgvalOLD  27881  opsqrlem3  31147  fedgmul  32413  mdetpmtr12  32495  madjusmdetlem4  32500  dya2iocival  32962  sxbrsigalem5  32977  sxbrsigalem6  32978  eulerpart  33071  sseqp1  33084  cvmliftlem15  33979  cvmlift2  33997  opnmbllem0  36187  mblfinlem1  36188  mblfinlem2  36189  sdc  36276  tendoplcbv  39311  dvhvaddcbv  39625  dvhvscacbv  39634  fsovcnvlem  42407  ntrneibex  42467  ioorrnopn  44666  hoidmvle  44961  ovnhoi  44964  hoimbl  44992  smflimlem6  45137  funcrngcsetc  46416  funcrngcsetcALT  46417  funcringcsetc  46453  lmod1zr  46694  functhinclem4  47184