Theorem weeq1 5568

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   Or wor 5493   Fr wfr 5532   We wwe 5534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-ex 1784  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-br 5071  df-po 5494  df-so 5495  df-fr 5535  df-we 5537

This theorem is referenced by:  oieq1  9201  hartogslem1  9231  wemapwe  9385  infxpenlem  9700  dfac8b  9718  ac10ct  9721  fpwwe2cbv  10317  fpwwe2lem2  10319  fpwwe2lem4  10321  fpwwecbv  10331  fpwwelem  10332  canthnumlem  10335  canthwelem  10337  canthwe  10338  canthp1lem2  10340  pwfseqlem4a  10348  pwfseqlem4  10349  ltbwe  21155  vitali  24682  fin2so  35691  weeq12d  40781  dnwech  40789  aomclem5  40799  aomclem6  40800  aomclem7  40801