HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem weeq1 2932
Description: Equality theorem for the well-ordering predicate.
Assertion
Ref Expression
weeq1 |- (R = S -> (R We A <-> S We A))
Proof of Theorem weeq1
StepHypRef Expression
1 freq1 2917 . . 3 |- (R = S -> (R Fr A <-> S Fr A))
2 soeq1 2848 . . 3 |- (R = S -> (R Or A <-> S Or A))
31, 2anbi12d 627 . 2 |- (R = S -> ((R Fr A /\ R Or A) <-> (S Fr A /\ S Or A)))
4 df-we 2929 . 2 |- (R We A <-> (R Fr A /\ R Or A))
5 df-we 2929 . 2 |- (S We A <-> (S Fr A /\ S Or A))
63, 4, 53bitr4g 554 1 |- (R = S -> (R We A <-> S We A))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 954   Or wor 2834   Fr wfr 2910   We wwe 2911
This theorem is referenced by:  weth 4767
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-ex 979  df-cleq 1467  df-clel 1470  df-ral 1646  df-rex 1647  df-br 2615  df-po 2835  df-so 2845  df-fr 2912  df-we 2929
Copyright terms: Public domain