Theorem weeq1 5345

Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)

Assertion

Ref	Expression
weeq1	⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴))

Proof of Theorem weeq1

Step	Hyp	Ref	Expression
1		freq1 5327	. . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴))
2		soeq1 5296	. . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴))
3	1, 2	anbi12d 624	. 2 ⊢ (𝑅 = 𝑆 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴)))
4		df-we 5318	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
5		df-we 5318	. 2 ⊢ (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴))
6	3, 4, 5	3bitr4g 306	1 ⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601   Or wor 5275   Fr wfr 5313   We wwe 5315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-ex 1824  df-cleq 2770  df-clel 2774  df-ral 3095  df-rex 3096  df-br 4889  df-po 5276  df-so 5277  df-fr 5316  df-we 5318

This theorem is referenced by:  oieq1  8708  hartogslem1  8738  wemapwe  8893  infxpenlem  9171  dfac8b  9189  ac10ct  9192  fpwwe2cbv  9789  fpwwe2lem2  9791  fpwwe2lem5  9793  fpwwecbv  9803  fpwwelem  9804  canthnumlem  9807  canthwelem  9809  canthwe  9810  canthp1lem2  9812  pwfseqlem4a  9820  pwfseqlem4  9821  ltbwe  19880  vitali  23828  fin2so  34030  weeq12d  38583  dnwech  38591  aomclem5  38601  aomclem6  38602  aomclem7  38603