Theorem soeq1 2859

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 2848	. . 3 ⊢ (R = S → (R Po A ↔ S Po A))
2		breq 2626	. . . . 5 ⊢ (R = S → (xRy ↔ xSy))
3		pm4.2d 171	. . . . 5 ⊢ (R = S → (x = y ↔ x = y))
4		breq 2626	. . . . 5 ⊢ (R = S → (yRx ↔ ySx))
5	2, 3, 4	3orbi123d 894	. . . 4 ⊢ (R = S → ((xRy ⋁ x = y ⋁ yRx) ↔ (xSy ⋁ x = y ⋁ ySx)))
6	5	2ralbidv 1683	. . 3 ⊢ (R = S → (∀x ∈ A ∀y ∈ A (xRy ⋁ x = y ⋁ yRx) ↔ ∀x ∈ A ∀y ∈ A (xSy ⋁ x = y ⋁ ySx)))
7	1, 6	anbi12d 630	. 2 ⊢ (R = S → ((R Po A ⋀ ∀x ∈ A ∀y ∈ A (xRy ⋁ x = y ⋁ yRx)) ↔ (S Po A ⋀ ∀x ∈ A ∀y ∈ A (xSy ⋁ x = y ⋁ ySx))))
8		df-so 2856	. 2 ⊢ (R Or A ↔ (R Po A ⋀ ∀x ∈ A ∀y ∈ A (xRy ⋁ x = y ⋁ yRx)))
9		df-so 2856	. 2 ⊢ (S Or A ↔ (S Po A ⋀ ∀x ∈ A ∀y ∈ A (xSy ⋁ x = y ⋁ ySx)))
10	7, 8, 9	3bitr4g 557	1 ⊢ (R = S → (R Or A ↔ S Or A))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   ⋁ w3o 776   = wceq 958  ∀wral 1648   class class class wbr 2624   Po wpo 2844   Or wor 2845

This theorem is referenced by:  weeq1 2943

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-ex 983  df-cleq 1472  df-clel 1475  df-ral 1652  df-br 2625  df-po 2846  df-so 2856

Copyright terms: Public domain