Theorem cbvmpov 7455

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

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-oprab 7364  df-mpo 7365

This theorem is referenced by:  fvproj  8077  seqomlem0  8381  dffi3  9337  cantnfsuc  9582  fin23lem33  10258  om2uzrdg  13909  uzrdgsuci  13913  sadcp1  16415  smupp1  16440  imasvscafn  17492  mgmnsgrpex  18893  sgrpnmndex  18894  sylow1  19569  sylow2b  19589  sylow3lem5  19597  sylow3  19599  efgmval  19678  efgtf  19688  funcrngcsetc  20608  funcrngcsetcALT  20609  funcringcsetc  20642  frlmphl  21771  pmatcollpw3lem  22758  mp2pm2mplem3  22783  txbas  23542  mpomulcn  24844  bcth  25306  opnmbl  25579  mbfimaopn  25633  mbfi1fseq  25698  om2noseqrdg  28310  noseqrdgsuc  28314  motplusg  28624  ttgval  28957  opsqrlem3  32228  elrgspnlem2  33319  splysubrg  33719  issply  33720  fedgmul  33791  mdetpmtr12  33985  madjusmdetlem4  33990  dya2iocival  34433  sxbrsigalem5  34448  sxbrsigalem6  34449  eulerpart  34542  sseqp1  34555  cvmliftlem15  35496  cvmlift2  35514  opnmbllem0  37991  mblfinlem1  37992  mblfinlem2  37993  sdc  38079  tendoplcbv  41235  dvhvaddcbv  41549  dvhvscacbv  41558  fsovcnvlem  44458  ntrneibex  44518  ioorrnopn  46751  hoidmvle  47046  ovnhoi  47049  hoimbl  47077  smflimlem6  47222  lmod1zr  48981  functhinclem4  49934