Theorem weeq1 5026

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 5008	. . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴))
2		soeq1 4978	. . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴))
3	1, 2	anbi12d 743	. 2 ⊢ (𝑅 = 𝑆 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴)))
4		df-we 4999	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
5		df-we 4999	. 2 ⊢ (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴))
6	3, 4, 5	3bitr4g 302	1 ⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   Or wor 4958   Fr wfr 4994   We wwe 4996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-ex 1696  df-cleq 2603  df-clel 2606  df-ral 2901  df-rex 2902  df-br 4584  df-po 4959  df-so 4960  df-fr 4997  df-we 4999

This theorem is referenced by:  oieq1  8300  hartogslem1  8330  wemapwe  8477  infxpenlem  8719  dfac8b  8737  ac10ct  8740  fpwwe2cbv  9331  fpwwe2lem2  9333  fpwwe2lem5  9335  fpwwecbv  9345  fpwwelem  9346  canthnumlem  9349  canthwelem  9351  canthwe  9352  canthp1lem2  9354  pwfseqlem4a  9362  pwfseqlem4  9363  ltbwe  19293  vitali  23188  fin2so  32566  weeq12d  36628  dnwech  36636  aomclem5  36646  aomclem6  36647  aomclem7  36648