MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvmpov Structured version   Visualization version   GIF version

Theorem cbvmpov 7528
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 5253, 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.
StepHypRef Expression
1 eleq1w 2824 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
2 eleq1w 2824 . . . . 5 (𝑦 = 𝑤 → (𝑦𝐵𝑤𝐵))
31, 2bi2anan9 638 . . . 4 ((𝑥 = 𝑧𝑦 = 𝑤) → ((𝑥𝐴𝑦𝐵) ↔ (𝑧𝐴𝑤𝐵)))
4 cbvmpov.1 . . . . . 6 (𝑥 = 𝑧𝐶 = 𝐸)
5 cbvmpov.2 . . . . . 6 (𝑦 = 𝑤𝐸 = 𝐷)
64, 5sylan9eq 2797 . . . . 5 ((𝑥 = 𝑧𝑦 = 𝑤) → 𝐶 = 𝐷)
76eqeq2d 2748 . . . 4 ((𝑥 = 𝑧𝑦 = 𝑤) → (𝑣 = 𝐶𝑣 = 𝐷))
83, 7anbi12d 632 . . 3 ((𝑥 = 𝑧𝑦 = 𝑤) → (((𝑥𝐴𝑦𝐵) ∧ 𝑣 = 𝐶) ↔ ((𝑧𝐴𝑤𝐵) ∧ 𝑣 = 𝐷)))
98cbvoprab12v 7523 . 2 {⟨⟨𝑥, 𝑦⟩, 𝑣⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑣 = 𝐶)} = {⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∣ ((𝑧𝐴𝑤𝐵) ∧ 𝑣 = 𝐷)}
10 df-mpo 7436 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑣⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑣 = 𝐶)}
11 df-mpo 7436 . 2 (𝑧𝐴, 𝑤𝐵𝐷) = {⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∣ ((𝑧𝐴𝑤𝐵) ∧ 𝑣 = 𝐷)}
129, 10, 113eqtr4i 2775 1 (𝑥𝐴, 𝑦𝐵𝐶) = (𝑧𝐴, 𝑤𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  {coprab 7432  cmpo 7433
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 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-oprab 7435  df-mpo 7436
This theorem is referenced by:  fvproj  8159  seqomlem0  8489  dffi3  9471  cantnfsuc  9710  fin23lem33  10385  om2uzrdg  13997  uzrdgsuci  14001  sadcp1  16492  smupp1  16517  imasvscafn  17582  mgmnsgrpex  18944  sgrpnmndex  18945  sylow1  19621  sylow2b  19641  sylow3lem5  19649  sylow3  19651  efgmval  19730  efgtf  19740  funcrngcsetc  20640  funcrngcsetcALT  20641  funcringcsetc  20674  frlmphl  21801  pmatcollpw3lem  22789  mp2pm2mplem3  22814  txbas  23575  mpomulcn  24891  bcth  25363  opnmbl  25637  mbfimaopn  25691  mbfi1fseq  25756  om2noseqrdg  28310  noseqrdgsuc  28314  motplusg  28550  ttgval  28883  ttgvalOLD  28884  opsqrlem3  32161  elrgspnlem2  33247  fedgmul  33682  mdetpmtr12  33824  madjusmdetlem4  33829  dya2iocival  34275  sxbrsigalem5  34290  sxbrsigalem6  34291  eulerpart  34384  sseqp1  34397  cvmliftlem15  35303  cvmlift2  35321  opnmbllem0  37663  mblfinlem1  37664  mblfinlem2  37665  sdc  37751  tendoplcbv  40777  dvhvaddcbv  41091  dvhvscacbv  41100  fsovcnvlem  44026  ntrneibex  44086  ioorrnopn  46320  hoidmvle  46615  ovnhoi  46618  hoimbl  46646  smflimlem6  46791  lmod1zr  48410  functhinclem4  49096
  Copyright terms: Public domain W3C validator