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  27793  ttgval  28126  ttgvalOLD  28127  opsqrlem3  31395  fedgmul  32716  mdetpmtr12  32805  madjusmdetlem4  32810  dya2iocival  33272  sxbrsigalem5  33287  sxbrsigalem6  33288  eulerpart  33381  sseqp1  33394  cvmliftlem15  34289  cvmlift2  34307  mpomulcn  35162  opnmbllem0  36524  mblfinlem1  36525  mblfinlem2  36526  sdc  36612  tendoplcbv  39646  dvhvaddcbv  39960  dvhvscacbv  39969  fsovcnvlem  42764  ntrneibex  42824  ioorrnopn  45021  hoidmvle  45316  ovnhoi  45319  hoimbl  45347  smflimlem6  45492  funcrngcsetc  46896  funcrngcsetcALT  46897  funcringcsetc  46933  lmod1zr  47174  functhinclem4  47664