Theorem weeq1 5542

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   Or wor 5472   Fr wfr 5510   We wwe 5512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-ex 1777  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144  df-br 5066  df-po 5473  df-so 5474  df-fr 5513  df-we 5515

This theorem is referenced by:  oieq1  8975  hartogslem1  9005  wemapwe  9159  infxpenlem  9438  dfac8b  9456  ac10ct  9459  fpwwe2cbv  10051  fpwwe2lem2  10053  fpwwe2lem5  10055  fpwwecbv  10065  fpwwelem  10066  canthnumlem  10069  canthwelem  10071  canthwe  10072  canthp1lem2  10074  pwfseqlem4a  10082  pwfseqlem4  10083  ltbwe  20252  vitali  24213  fin2so  34878  weeq12d  39638  dnwech  39646  aomclem5  39656  aomclem6  39657  aomclem7  39658