Theorem cbvmpov 7402

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

Syntax hints:   → wi 4   = wceq 1539   ∈ cmpo 7309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-opab 5144  df-oprab 7311  df-mpo 7312

This theorem is referenced by:  fvproj  8006  seqomlem0  8311  dffi3  9234  cantnfsuc  9472  fin23lem33  10147  om2uzrdg  13722  uzrdgsuci  13726  sadcp1  16207  smupp1  16232  imasvscafn  17293  mgmnsgrpex  18615  sgrpnmndex  18616  sylow1  19253  sylow2b  19273  sylow3lem5  19281  sylow3  19283  efgmval  19363  efgtf  19373  frlmphl  21033  pmatcollpw3lem  21977  mp2pm2mplem3  22002  txbas  22763  bcth  24538  opnmbl  24811  mbfimaopn  24865  mbfi1fseq  24931  motplusg  26948  ttgval  27281  ttgvalOLD  27282  opsqrlem3  30549  fedgmul  31757  mdetpmtr12  31820  madjusmdetlem4  31825  dya2iocival  32285  sxbrsigalem5  32300  sxbrsigalem6  32301  eulerpart  32394  sseqp1  32407  cvmliftlem15  33305  cvmlift2  33323  opnmbllem0  35857  mblfinlem1  35858  mblfinlem2  35859  sdc  35946  tendoplcbv  38831  dvhvaddcbv  39145  dvhvscacbv  39154  fsovcnvlem  41659  ntrneibex  41721  ioorrnopn  43895  hoidmvle  44188  ovnhoi  44191  hoimbl  44219  smflimlem6  44364  funcrngcsetc  45614  funcrngcsetcALT  45615  funcringcsetc  45651  lmod1zr  45892  functhinclem4  46383