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

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

Proof of Theorem mpt2eq12
StepHypRef Expression
1 eqid 2621 . . . . 5 𝐸 = 𝐸
21rgenw 2920 . . . 4 𝑦𝐵 𝐸 = 𝐸
32jctr 564 . . 3 (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸))
43ralrimivw 2963 . 2 (𝐵 = 𝐷 → ∀𝑥𝐴 (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸))
5 mpt2eq123 6679 . 2 ((𝐴 = 𝐶 ∧ ∀𝑥𝐴 (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸)) → (𝑥𝐴, 𝑦𝐵𝐸) = (𝑥𝐶, 𝑦𝐷𝐸))
64, 5sylan2 491 1 ((𝐴 = 𝐶𝐵 = 𝐷) → (𝑥𝐴, 𝑦𝐵𝐸) = (𝑥𝐶, 𝑦𝐷𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wral 2908  cmpt2 6617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-oprab 6619  df-mpt2 6620
This theorem is referenced by:  dffi3  8297  cantnfres  8534  xpsval  16172  homffval  16290  comfffval  16298  monpropd  16337  natfval  16546  plusffval  17187  grpsubfval  17404  grpsubpropd2  17461  lsmvalx  17994  oppglsm  17997  lsmpropd  18030  dvrfval  18624  scaffval  18821  psrmulr  19324  psrplusgpropd  19546  ipffval  19933  marrepfval  20306  marepvfval  20311  d1mat2pmat  20484  txval  21307  cnmptk1p  21428  cnmptk2  21429  xpstopnlem1  21552  pcofval  22750  rrxmval  23128  madjusmdetlem1  29717  pstmval  29762  qqhval2  29850  mendplusgfval  37275  mendmulrfval  37277  mendvscafval  37280  funcrngcsetc  41316  funcringcsetc  41353  lmod1zr  41600
  Copyright terms: Public domain W3C validator