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

Theorem s1eqd 12587
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 12586 . 2  |-  ( A  =  B  ->  <" A ">  =  <" B "> )
31, 2syl 16 1  |-  ( ph  ->  <" A ">  =  <" B "> )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381   <"cs1 12511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-iota 5537  df-fv 5582  df-s1 12519
This theorem is referenced by:  swrds1  12650  swrdlsw  12651  swrdccatwrd  12667  s2eqd  12801  s3eqd  12802  s4eqd  12803  s5eqd  12804  s6eqd  12805  s7eqd  12806  s8eqd  12807  frmdgsum  15899  psgnunilem5  16388  efgredlemc  16632  vrgpval  16654  vrgpinv  16656  frgpup2  16663  frgpup3lem  16664  iwrdsplit  28192  sseqval  28193  sseqf  28197  sseqp1  28200  signsvtn0  28393  mrsubcv  28736
  Copyright terms: Public domain W3C validator