Theorem weeq1 5545

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   Or wor 5475   Fr wfr 5513   We wwe 5515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-ex 1781  df-cleq 2816  df-clel 2895  df-ral 3145  df-rex 3146  df-br 5069  df-po 5476  df-so 5477  df-fr 5516  df-we 5518

This theorem is referenced by:  oieq1  8978  hartogslem1  9008  wemapwe  9162  infxpenlem  9441  dfac8b  9459  ac10ct  9462  fpwwe2cbv  10054  fpwwe2lem2  10056  fpwwe2lem5  10058  fpwwecbv  10068  fpwwelem  10069  canthnumlem  10072  canthwelem  10074  canthwe  10075  canthp1lem2  10077  pwfseqlem4a  10085  pwfseqlem4  10086  ltbwe  20255  vitali  24216  fin2so  34881  weeq12d  39647  dnwech  39655  aomclem5  39665  aomclem6  39666  aomclem7  39667