Theorem cbvmpov 7488

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 5252, 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 7487	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)

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

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 5292  ax-nul 5299  ax-pr 5420

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 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-opab 5204  df-oprab 7397  df-mpo 7398

This theorem is referenced by:  fvproj  8102  seqomlem0  8431  dffi3  9408  cantnfsuc  9647  fin23lem33  10322  om2uzrdg  13903  uzrdgsuci  13907  sadcp1  16378  smupp1  16403  imasvscafn  17465  mgmnsgrpex  18787  sgrpnmndex  18788  sylow1  19435  sylow2b  19455  sylow3lem5  19463  sylow3  19465  efgmval  19544  efgtf  19554  frlmphl  21269  pmatcollpw3lem  22214  mp2pm2mplem3  22239  txbas  23000  bcth  24775  opnmbl  25048  mbfimaopn  25102  mbfi1fseq  25168  motplusg  27658  ttgval  27991  ttgvalOLD  27992  opsqrlem3  31258  fedgmul  32554  mdetpmtr12  32636  madjusmdetlem4  32641  dya2iocival  33103  sxbrsigalem5  33118  sxbrsigalem6  33119  eulerpart  33212  sseqp1  33225  cvmliftlem15  34120  cvmlift2  34138  opnmbllem0  36328  mblfinlem1  36329  mblfinlem2  36330  sdc  36417  tendoplcbv  39451  dvhvaddcbv  39765  dvhvscacbv  39774  fsovcnvlem  42535  ntrneibex  42595  ioorrnopn  44794  hoidmvle  45089  ovnhoi  45092  hoimbl  45120  smflimlem6  45265  funcrngcsetc  46544  funcrngcsetcALT  46545  funcringcsetc  46581  lmod1zr  46822  functhinclem4  47312