Theorem weeq1 5654

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 5636	. . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴))
2		soeq1 5599	. . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴))
3	1, 2	anbi12d 630	. 2 ⊢ (𝑅 = 𝑆 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴)))
4		df-we 5623	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
5		df-we 5623	. 2 ⊢ (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   Or wor 5577   Fr wfr 5618   We wwe 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-ex 1774  df-cleq 2716  df-clel 2802  df-ral 3054  df-rex 3063  df-br 5139  df-po 5578  df-so 5579  df-fr 5621  df-we 5623

This theorem is referenced by:  oieq1  9503  hartogslem1  9533  wemapwe  9688  infxpenlem  10004  dfac8b  10022  ac10ct  10025  fpwwe2cbv  10621  fpwwe2lem2  10623  fpwwe2lem4  10625  fpwwecbv  10635  fpwwelem  10636  canthnumlem  10639  canthwelem  10641  canthwe  10642  canthp1lem2  10644  pwfseqlem4a  10652  pwfseqlem4  10653  ltbwe  21909  vitali  25464  fin2so  36965  weeq12d  42271  dnwech  42279  aomclem5  42289  aomclem6  42290  aomclem7  42291