Theorem weeq1 5507

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 5489	. . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴))
2		soeq1 5458	. . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴))
3	1, 2	anbi12d 633	. 2 ⊢ (𝑅 = 𝑆 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴)))
4		df-we 5480	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
5		df-we 5480	. 2 ⊢ (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   Or wor 5437   Fr wfr 5475   We wwe 5477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-ex 1782  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-br 5031  df-po 5438  df-so 5439  df-fr 5478  df-we 5480

This theorem is referenced by:  oieq1  8960  hartogslem1  8990  wemapwe  9144  infxpenlem  9424  dfac8b  9442  ac10ct  9445  fpwwe2cbv  10041  fpwwe2lem2  10043  fpwwe2lem5  10045  fpwwecbv  10055  fpwwelem  10056  canthnumlem  10059  canthwelem  10061  canthwe  10062  canthp1lem2  10064  pwfseqlem4a  10072  pwfseqlem4  10073  ltbwe  20712  vitali  24217  fin2so  35044  weeq12d  39984  dnwech  39992  aomclem5  40002  aomclem6  40003  aomclem7  40004