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

Theorem mpoeq12 7368
Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
Assertion
Ref Expression
mpoeq12 ((𝐴 = 𝐶𝐵 = 𝐷) → (𝑥𝐴, 𝑦𝐵𝐸) = (𝑥𝐶, 𝑦𝐷𝐸))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦
Allowed substitution hints:   𝐸(𝑥,𝑦)

Proof of Theorem mpoeq12
StepHypRef Expression
1 eqid 2733 . . . . 5 𝐸 = 𝐸
21rgenw 3063 . . . 4 𝑦𝐵 𝐸 = 𝐸
32jctr 524 . . 3 (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸))
43ralrimivw 3141 . 2 (𝐵 = 𝐷 → ∀𝑥𝐴 (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸))
5 mpoeq123 7367 . 2 ((𝐴 = 𝐶 ∧ ∀𝑥𝐴 (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸)) → (𝑥𝐴, 𝑦𝐵𝐸) = (𝑥𝐶, 𝑦𝐷𝐸))
64, 5sylan2 592 1 ((𝐴 = 𝐶𝐵 = 𝐷) → (𝑥𝐴, 𝑦𝐵𝐸) = (𝑥𝐶, 𝑦𝐷𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wral 3059  cmpo 7297
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-10 2132  ax-11 2149  ax-12 2166  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2884  df-ral 3060  df-oprab 7299  df-mpo 7300
This theorem is referenced by:  dffi3  9218  cantnfres  9463  xpsval  17309  monpropd  17477  grpsubpropd2  18709  lsmvalx  19272  lsmpropd  19311  psrplusgpropd  21435  d1mat2pmat  21916  txval  22743  cnmptk1p  22864  cnmptk2  22865  xpstopnlem1  22988  rrxmval  24597  madjusmdetlem1  31805  pstmval  31873  qqhval2  31960  funcrngcsetc  45596  funcringcsetc  45633  lmod1zr  45874
  Copyright terms: Public domain W3C validator