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 5259, 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 2822 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
2 eleq1w 2822 . . . . 5 (𝑦 = 𝑤 → (𝑦𝐵𝑤𝐵))
31, 2bi2anan9 638 . . . 4 ((𝑥 = 𝑧𝑦 = 𝑤) → ((𝑥𝐴𝑦𝐵) ↔ (𝑧𝐴𝑤𝐵)))
4 cbvmpov.1 . . . . . 6 (𝑥 = 𝑧𝐶 = 𝐸)
5 cbvmpov.2 . . . . . 6 (𝑦 = 𝑤𝐸 = 𝐷)
64, 5sylan9eq 2795 . . . . 5 ((𝑥 = 𝑧𝑦 = 𝑤) → 𝐶 = 𝐷)
76eqeq2d 2746 . . . 4 ((𝑥 = 𝑧𝑦 = 𝑤) → (𝑣 = 𝐶𝑣 = 𝐷))
83, 7anbi12d 632 . . 3 ((𝑥 = 𝑧𝑦 = 𝑤) → (((𝑥𝐴𝑦𝐵) ∧ 𝑣 = 𝐶) ↔ ((𝑧𝐴𝑤𝐵) ∧ 𝑣 = 𝐷)))
98cbvoprab12v 7523 . 2 {⟨⟨𝑥, 𝑦⟩, 𝑣⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑣 = 𝐶)} = {⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∣ ((𝑧𝐴𝑤𝐵) ∧ 𝑣 = 𝐷)}
10 df-mpo 7436 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑣⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑣 = 𝐶)}
11 df-mpo 7436 . 2 (𝑧𝐴, 𝑤𝐵𝐷) = {⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∣ ((𝑧𝐴𝑤𝐵) ∧ 𝑣 = 𝐷)}
129, 10, 113eqtr4i 2773 1 (𝑥𝐴, 𝑦𝐵𝐶) = (𝑧𝐴, 𝑤𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wcel 2106  {coprab 7432  cmpo 7433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-oprab 7435  df-mpo 7436
This theorem is referenced by:  fvproj  8158  seqomlem0  8488  dffi3  9469  cantnfsuc  9708  fin23lem33  10383  om2uzrdg  13994  uzrdgsuci  13998  sadcp1  16489  smupp1  16514  imasvscafn  17584  mgmnsgrpex  18957  sgrpnmndex  18958  sylow1  19636  sylow2b  19656  sylow3lem5  19664  sylow3  19666  efgmval  19745  efgtf  19755  funcrngcsetc  20657  funcrngcsetcALT  20658  funcringcsetc  20691  frlmphl  21819  pmatcollpw3lem  22805  mp2pm2mplem3  22830  txbas  23591  mpomulcn  24905  bcth  25377  opnmbl  25651  mbfimaopn  25705  mbfi1fseq  25771  om2noseqrdg  28325  noseqrdgsuc  28329  motplusg  28565  ttgval  28898  ttgvalOLD  28899  opsqrlem3  32171  elrgspnlem2  33233  fedgmul  33659  mdetpmtr12  33786  madjusmdetlem4  33791  dya2iocival  34255  sxbrsigalem5  34270  sxbrsigalem6  34271  eulerpart  34364  sseqp1  34377  cvmliftlem15  35283  cvmlift2  35301  opnmbllem0  37643  mblfinlem1  37644  mblfinlem2  37645  sdc  37731  tendoplcbv  40758  dvhvaddcbv  41072  dvhvscacbv  41081  fsovcnvlem  44003  ntrneibex  44063  ioorrnopn  46261  hoidmvle  46556  ovnhoi  46559  hoimbl  46587  smflimlem6  46732  lmod1zr  48339  functhinclem4  48844
  Copyright terms: Public domain W3C validator