Theorem weeq1 5654

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   Or wor 5573   Fr wfr 5616   We wwe 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-ex 1779  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-br 5126  df-po 5574  df-so 5575  df-fr 5619  df-we 5621

This theorem is referenced by:  weeq12d  5656  oieq1  9535  hartogslem1  9565  wemapwe  9720  infxpenlem  10036  dfac8b  10054  ac10ct  10057  canthnumlem  10671  canthp1lem2  10676  pwfseqlem4a  10684  pwfseqlem4  10685  ltbwe  22029  vitali  25603  numiunnum  36412  fin2so  37555  dnwech  43005  aomclem5  43015  aomclem6  43016  aomclem7  43017