Theorem cbvmpov 7462

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 5187, 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 2819	. . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
2		eleq1w 2819	. . . . 5 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵))
3	1, 2	bi2anan9 639	. . . 4 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)))
4		cbvmpov.1	. . . . . 6 ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)
5		cbvmpov.2	. . . . . 6 ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷)
6	4, 5	sylan9eq 2791	. . . . 5 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)
7	6	eqeq2d 2747	. . . 4 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑣 = 𝐶 ↔ 𝑣 = 𝐷))
8	3, 7	anbi12d 633	. . 3 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷)))
9	8	cbvoprab12v 7457	. 2 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑣⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} = {⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷)}
10		df-mpo 7372	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑣⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)}
11		df-mpo 7372	. 2 ⊢ (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷)}
12	9, 10, 11	3eqtr4i 2769	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {coprab 7368   ∈ cmpo 7369

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-oprab 7371  df-mpo 7372

This theorem is referenced by:  fvproj  8084  seqomlem0  8388  dffi3  9344  cantnfsuc  9591  fin23lem33  10267  om2uzrdg  13918  uzrdgsuci  13922  sadcp1  16424  smupp1  16449  imasvscafn  17501  mgmnsgrpex  18902  sgrpnmndex  18903  sylow1  19578  sylow2b  19598  sylow3lem5  19606  sylow3  19608  efgmval  19687  efgtf  19697  funcrngcsetc  20617  funcrngcsetcALT  20618  funcringcsetc  20651  frlmphl  21761  pmatcollpw3lem  22748  mp2pm2mplem3  22773  txbas  23532  mpomulcn  24834  bcth  25296  opnmbl  25569  mbfimaopn  25623  mbfi1fseq  25688  om2noseqrdg  28296  noseqrdgsuc  28300  motplusg  28610  ttgval  28943  opsqrlem3  32213  elrgspnlem2  33304  splysubrg  33704  issply  33705  fedgmul  33775  mdetpmtr12  33969  madjusmdetlem4  33974  dya2iocival  34417  sxbrsigalem5  34432  sxbrsigalem6  34433  eulerpart  34526  sseqp1  34539  cvmliftlem15  35480  cvmlift2  35498  opnmbllem0  37977  mblfinlem1  37978  mblfinlem2  37979  sdc  38065  tendoplcbv  41221  dvhvaddcbv  41535  dvhvscacbv  41544  fsovcnvlem  44440  ntrneibex  44500  ioorrnopn  46733  hoidmvle  47028  ovnhoi  47031  hoimbl  47059  smflimlem6  47204  lmod1zr  48969  functhinclem4  49922