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

Theorem mpoeq12 7206
 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 2798 . . . . 5 𝐸 = 𝐸
21rgenw 3118 . . . 4 𝑦𝐵 𝐸 = 𝐸
32jctr 528 . . 3 (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸))
43ralrimivw 3150 . 2 (𝐵 = 𝐷 → ∀𝑥𝐴 (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸))
5 mpoeq123 7205 . 2 ((𝐴 = 𝐶 ∧ ∀𝑥𝐴 (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸)) → (𝑥𝐴, 𝑦𝐵𝐸) = (𝑥𝐶, 𝑦𝐷𝐸))
64, 5sylan2 595 1 ((𝐴 = 𝐶𝐵 = 𝐷) → (𝑥𝐴, 𝑦𝐵𝐸) = (𝑥𝐶, 𝑦𝐷𝐸))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  ∀wral 3106   ∈ cmpo 7137 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-oprab 7139  df-mpo 7140 This theorem is referenced by:  dffi3  8881  cantnfres  9126  xpsval  16837  monpropd  17001  grpsubpropd2  18200  lsmvalx  18759  lsmpropd  18798  psrplusgpropd  20872  d1mat2pmat  21351  txval  22176  cnmptk1p  22297  cnmptk2  22298  xpstopnlem1  22421  rrxmval  24016  madjusmdetlem1  31192  pstmval  31260  qqhval2  31345  funcrngcsetc  44637  funcringcsetc  44674  lmod1zr  44916
 Copyright terms: Public domain W3C validator