Theorem weeq1 5649

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   Or wor 5569   Fr wfr 5612   We wwe 5614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-ex 1807  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-br 5114  df-po 5570  df-so 5571  df-fr 5615  df-we 5617

This theorem is referenced by:  weeq12d  5651  oieq1  9474  hartogslem1  9504  wemapwe  9666  infxpenlem  9997  dfac8b  10015  ac10ct  10018  canthnumlem  10633  canthp1lem2  10638  pwfseqlem4a  10646  pwfseqlem4  10647  ltbwe  22164  vitali  25741  numiunnum  36904  fin2so  38180  dnwech  43701  aomclem5  43711  aomclem6  43712  aomclem7  43713