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

Theorem mpoeq12 7092
 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 2797 . . . . 5 𝐸 = 𝐸
21rgenw 3119 . . . 4 𝑦𝐵 𝐸 = 𝐸
32jctr 525 . . 3 (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸))
43ralrimivw 3152 . 2 (𝐵 = 𝐷 → ∀𝑥𝐴 (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸))
5 mpoeq123 7091 . 2 ((𝐴 = 𝐶 ∧ ∀𝑥𝐴 (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸)) → (𝑥𝐴, 𝑦𝐵𝐸) = (𝑥𝐶, 𝑦𝐷𝐸))
64, 5sylan2 592 1 ((𝐴 = 𝐶𝐵 = 𝐷) → (𝑥𝐴, 𝑦𝐵𝐸) = (𝑥𝐶, 𝑦𝐷𝐸))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   = wceq 1525  ∀wral 3107   ∈ cmpo 7025 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-oprab 7027  df-mpo 7028 This theorem is referenced by:  dffi3  8748  cantnfres  8993  xpsval  16676  homffval  16793  comfffval  16801  monpropd  16840  natfval  17049  plusffval  17690  grpsubfval  17908  grpsubfvalALT  17909  grpsubpropd2  17966  lsmvalx  18498  oppglsm  18501  lsmpropd  18534  dvrfval  19128  scaffval  19346  psrmulr  19856  psrplusgpropd  20091  ipffval  20478  marrepfval  20857  marepvfval  20862  d1mat2pmat  21035  txval  21860  cnmptk1p  21981  cnmptk2  21982  xpstopnlem1  22105  pcofval  23301  rrxmval  23695  madjusmdetlem1  30703  pstmval  30748  qqhval2  30836  mendplusgfval  39291  mendmulrfval  39293  mendvscafval  39296  funcrngcsetc  43769  funcringcsetc  43806  lmod1zr  44050
 Copyright terms: Public domain W3C validator