Theorem weeq1 5514

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542   Or wor 5442   Fr wfr 5481   We wwe 5483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-ex 1787  df-cleq 2731  df-clel 2812  df-ral 3059  df-rex 3060  df-br 5032  df-po 5443  df-so 5444  df-fr 5484  df-we 5486

This theorem is referenced by:  oieq1  9052  hartogslem1  9082  wemapwe  9236  infxpenlem  9516  dfac8b  9534  ac10ct  9537  fpwwe2cbv  10133  fpwwe2lem2  10135  fpwwe2lem4  10137  fpwwecbv  10147  fpwwelem  10148  canthnumlem  10151  canthwelem  10153  canthwe  10154  canthp1lem2  10156  pwfseqlem4a  10164  pwfseqlem4  10165  ltbwe  20858  vitali  24368  fin2so  35410  weeq12d  40460  dnwech  40468  aomclem5  40478  aomclem6  40479  aomclem7  40480