Theorem cbvmpov 7515

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {coprab 7421   ∈ cmpo 7422

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-oprab 7424  df-mpo 7425

This theorem is used by:  fvproj  8153  seqomlem0  8462  dffi3  9426  cantnfsuc  9674  fin23lem33  10426  om2uzrdg  14102  uzrdgsuci  14106  sadcp1  16630  smupp1  16655  imasvscafn  17714  mgmnsgrpex  19135  sgrpnmndex  19136  sylow1  19822  sylow2b  19842  sylow3lem5  19850  sylow3  19852  efgmval  19931  efgtf  19941  funcrngcsetc  20897  funcrngcsetcALT  20898  funcringcsetc  20931  frlmphl  22092  pmatcollpw3lem  23106  mp2pm2mplem3  23131  txbas  23891  mpomulcn  25193  bcth  25655  opnmbl  25928  mbfimaopn  25982  mbfi1fseq  26047  om2noseqrdg  28695  noseqrdgsuc  28699  motplusg  29010  ttgval  29457  opsqrlem3  32749  elrgspnlem2  33850  splysubrg  34238  issply  34239  fedgmul  34309  mdetpmtr12  34503  madjusmdetlem4  34508  dya2iocival  34951  sxbrsigalem5  34966  sxbrsigalem6  34967  eulerpart  35060  sseqp1  35073  cvmliftlem15  36149  cvmlift2  36167  opnmbllem0  38667  mblfinlem1  38668  mblfinlem2  38669  sdc  38771  tendoplcbv  41925  dvhvaddcbv  42239  dvhvscacbv  42248  fsovcnvlem  45106  ntrneibex  45166  ioorrnopn  47408  hoidmvle  47703  ovnhoi  47706  hoimbl  47734  smflimlem6  47879  lmod1zr  49698  functhinclem4  50675  veronesematbasd  51148  veronesematrowd  51149  veroquadmodzerod  51152  veroquadnolindfd  51153  veroquaddetzerod  51154