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

Theorem mpt2eq12 6872
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 2752 . . . . 5 𝐸 = 𝐸
21rgenw 3054 . . . 4 𝑦𝐵 𝐸 = 𝐸
32jctr 566 . . 3 (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸))
43ralrimivw 3097 . 2 (𝐵 = 𝐷 → ∀𝑥𝐴 (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸))
5 mpt2eq123 6871 . 2 ((𝐴 = 𝐶 ∧ ∀𝑥𝐴 (𝐵 = 𝐷 ∧ ∀𝑦𝐵 𝐸 = 𝐸)) → (𝑥𝐴, 𝑦𝐵𝐸) = (𝑥𝐶, 𝑦𝐷𝐸))
64, 5sylan2 492 1 ((𝐴 = 𝐶𝐵 = 𝐷) → (𝑥𝐴, 𝑦𝐵𝐸) = (𝑥𝐶, 𝑦𝐷𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1624  wral 3042  cmpt2 6807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-oprab 6809  df-mpt2 6810
This theorem is referenced by:  dffi3  8494  cantnfres  8739  xpsval  16426  homffval  16543  comfffval  16551  monpropd  16590  natfval  16799  plusffval  17440  grpsubfval  17657  grpsubpropd2  17714  lsmvalx  18246  oppglsm  18249  lsmpropd  18282  dvrfval  18876  scaffval  19075  psrmulr  19578  psrplusgpropd  19800  ipffval  20187  marrepfval  20560  marepvfval  20565  d1mat2pmat  20738  txval  21561  cnmptk1p  21682  cnmptk2  21683  xpstopnlem1  21806  pcofval  23002  rrxmval  23380  madjusmdetlem1  30194  pstmval  30239  qqhval2  30327  mendplusgfval  38249  mendmulrfval  38251  mendvscafval  38254  funcrngcsetc  42500  funcringcsetc  42537  lmod1zr  42784
  Copyright terms: Public domain W3C validator