Theorem weeq1 5577

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   Or wor 5502   Fr wfr 5541   We wwe 5543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-ex 1783  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-br 5075  df-po 5503  df-so 5504  df-fr 5544  df-we 5546

This theorem is referenced by:  oieq1  9271  hartogslem1  9301  wemapwe  9455  infxpenlem  9769  dfac8b  9787  ac10ct  9790  fpwwe2cbv  10386  fpwwe2lem2  10388  fpwwe2lem4  10390  fpwwecbv  10400  fpwwelem  10401  canthnumlem  10404  canthwelem  10406  canthwe  10407  canthp1lem2  10409  pwfseqlem4a  10417  pwfseqlem4  10418  ltbwe  21245  vitali  24777  fin2so  35764  weeq12d  40865  dnwech  40873  aomclem5  40883  aomclem6  40884  aomclem7  40885