MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tposeqd Structured version   Unicode version

Theorem tposeqd 6834
Description: Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.)
Hypothesis
Ref Expression
tposeqd.1  |-  ( ph  ->  F  =  G )
Assertion
Ref Expression
tposeqd  |-  ( ph  -> tpos  F  = tpos  G )

Proof of Theorem tposeqd
StepHypRef Expression
1 tposeqd.1 . 2  |-  ( ph  ->  F  =  G )
2 tposeq 6833 . 2  |-  ( F  =  G  -> tpos  F  = tpos 
G )
31, 2syl 16 1  |-  ( ph  -> tpos  F  = tpos  G )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370  tpos ctpos 6830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4497  ax-nul 4505  ax-pr 4615
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3056  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-nul 3722  df-if 3876  df-sn 3962  df-pr 3964  df-op 3968  df-br 4377  df-opab 4435  df-mpt 4436  df-xp 4930  df-rel 4931  df-cnv 4932  df-co 4933  df-dm 4934  df-res 4936  df-tpos 6831
This theorem is referenced by:  oppcval  14740  oppchomfval  14741  oppccofval  14743  oppchomfpropd  14753  oppcmon  14765  oppgval  15950  oppgplusfval  15951  oppglsm  16231  opprval  16808  opprmulfval  16809  mattposvs  18436  mattpos1  18437  mamutpos  18440  mattposm  18441  madulid  18553
  Copyright terms: Public domain W3C validator