Theorem cbvmpov 7502

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 5223, 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

Dummy variable 𝑣 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1w 2817	. . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
2		eleq1w 2817	. . . . 5 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵))
3	1, 2	bi2anan9 638	. . . 4 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)))
4		cbvmpov.1	. . . . . 6 ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)
5		cbvmpov.2	. . . . . 6 ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷)
6	4, 5	sylan9eq 2790	. . . . 5 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)
7	6	eqeq2d 2746	. . . 4 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑣 = 𝐶 ↔ 𝑣 = 𝐷))
8	3, 7	anbi12d 632	. . 3 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷)))
9	8	cbvoprab12v 7497	. 2 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑣⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} = {⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷)}
10		df-mpo 7410	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑣⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)}
11		df-mpo 7410	. 2 ⊢ (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷)}
12	9, 10, 11	3eqtr4i 2768	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {coprab 7406   ∈ cmpo 7407

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-oprab 7409  df-mpo 7410

This theorem is referenced by:  fvproj  8133  seqomlem0  8463  dffi3  9443  cantnfsuc  9684  fin23lem33  10359  om2uzrdg  13974  uzrdgsuci  13978  sadcp1  16474  smupp1  16499  imasvscafn  17551  mgmnsgrpex  18909  sgrpnmndex  18910  sylow1  19584  sylow2b  19604  sylow3lem5  19612  sylow3  19614  efgmval  19693  efgtf  19703  funcrngcsetc  20600  funcrngcsetcALT  20601  funcringcsetc  20634  frlmphl  21741  pmatcollpw3lem  22721  mp2pm2mplem3  22746  txbas  23505  mpomulcn  24809  bcth  25281  opnmbl  25555  mbfimaopn  25609  mbfi1fseq  25674  om2noseqrdg  28250  noseqrdgsuc  28254  motplusg  28521  ttgval  28854  opsqrlem3  32123  elrgspnlem2  33238  fedgmul  33671  mdetpmtr12  33856  madjusmdetlem4  33861  dya2iocival  34305  sxbrsigalem5  34320  sxbrsigalem6  34321  eulerpart  34414  sseqp1  34427  cvmliftlem15  35320  cvmlift2  35338  opnmbllem0  37680  mblfinlem1  37681  mblfinlem2  37682  sdc  37768  tendoplcbv  40794  dvhvaddcbv  41108  dvhvscacbv  41117  fsovcnvlem  44037  ntrneibex  44097  ioorrnopn  46334  hoidmvle  46629  ovnhoi  46632  hoimbl  46660  smflimlem6  46805  lmod1zr  48469  functhinclem4  49333