Theorem cbvmpov 7504

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

Syntax hints:   → wi 4   = wceq 1542   ∈ cmpo 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-opab 5212  df-oprab 7413  df-mpo 7414

This theorem is referenced by:  fvproj  8120  seqomlem0  8449  dffi3  9426  cantnfsuc  9665  fin23lem33  10340  om2uzrdg  13921  uzrdgsuci  13925  sadcp1  16396  smupp1  16421  imasvscafn  17483  mgmnsgrpex  18812  sgrpnmndex  18813  sylow1  19471  sylow2b  19491  sylow3lem5  19499  sylow3  19501  efgmval  19580  efgtf  19590  frlmphl  21336  pmatcollpw3lem  22285  mp2pm2mplem3  22310  txbas  23071  bcth  24846  opnmbl  25119  mbfimaopn  25173  mbfi1fseq  25239  motplusg  27824  ttgval  28157  ttgvalOLD  28158  opsqrlem3  31426  fedgmul  32747  mdetpmtr12  32836  madjusmdetlem4  32841  dya2iocival  33303  sxbrsigalem5  33318  sxbrsigalem6  33319  eulerpart  33412  sseqp1  33425  cvmliftlem15  34320  cvmlift2  34338  mpomulcn  35193  opnmbllem0  36572  mblfinlem1  36573  mblfinlem2  36574  sdc  36660  tendoplcbv  39694  dvhvaddcbv  40008  dvhvscacbv  40017  fsovcnvlem  42812  ntrneibex  42872  ioorrnopn  45069  hoidmvle  45364  ovnhoi  45367  hoimbl  45395  smflimlem6  45540  funcrngcsetc  46944  funcrngcsetcALT  46945  funcringcsetc  46981  lmod1zr  47222  functhinclem4  47712