Theorem soeq1 2853

Description: Equality theorem for the strict ordering predicate.

Assertion

Ref	Expression
soeq1	|- (R = S -> (R Or A <-> S Or A))

Proof of Theorem soeq1

Step	Hyp	Ref	Expression
1		poeq1 2842	. . 3 |- (R = S -> (R Po A <-> S Po A))
2		breq 2621	. . . . 5 |- (R = S -> (xRy <-> xSy))
3		pm4.2d 171	. . . . 5 |- (R = S -> (x = y <-> x = y))
4		breq 2621	. . . . 5 |- (R = S -> (yRx <-> ySx))
5	2, 3, 4	3orbi123d 892	. . . 4 |- (R = S -> ((xRy \/ x = y \/ yRx) <-> (xSy \/ x = y \/ ySx)))
6	5	2ralbidv 1680	. . 3 |- (R = S -> (A.x e. A A.y e. A (xRy \/ x = y \/ yRx) <-> A.x e. A A.y e. A (xSy \/ x = y \/ ySx)))
7	1, 6	anbi12d 628	. 2 |- (R = S -> ((R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)) <-> (S Po A /\ A.x e. A A.y e. A (xSy \/ x = y \/ ySx))))
8		df-so 2850	. 2 |- (R Or A <-> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
9		df-so 2850	. 2 |- (S Or A <-> (S Po A /\ A.x e. A A.y e. A (xSy \/ x = y \/ ySx)))
10	7, 8, 9	3bitr4g 555	1 |- (R = S -> (R Or A <-> S Or A))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   \/ w3o 774   = wceq 956  A.wral 1645   class class class wbr 2619   Po wpo 2838   Or wor 2839

This theorem is referenced by:  weeq1 2937

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 776  df-ex 981  df-cleq 1469  df-clel 1472  df-ral 1649  df-br 2620  df-po 2840  df-so 2850

Copyright terms: Public domain