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

Theorem s1eqd 11536
Description: Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
Hypothesis
Ref Expression
s1eqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
s1eqd  |-  ( ph  ->  <" A ">  =  <" B "> )

Proof of Theorem s1eqd
StepHypRef Expression
1 s1eqd.1 . 2  |-  ( ph  ->  A  =  B )
2 s1eq 11535 . 2  |-  ( A  =  B  ->  <" A ">  =  <" B "> )
31, 2syl 15 1  |-  ( ph  ->  <" A ">  =  <" B "> )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642   <"cs1 11501
This theorem is referenced by:  swrds1  11569  s2eqd  11608  s3eqd  11609  s4eqd  11610  s5eqd  11611  s6eqd  11612  s7eqd  11613  s8eqd  11614  frmdgsum  14583  efgredlemc  15153  vrgpval  15175  vrgpinv  15177  frgpup2  15184  frgpup3lem  15185  psgnunilem5  26740
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-iota 5301  df-fv 5345  df-s1 11507
  Copyright terms: Public domain W3C validator