Theorem weeq1 5637

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   Or wor 5557   Fr wfr 5600   We wwe 5602

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-ex 1812  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-br 5103  df-po 5558  df-so 5559  df-fr 5603  df-we 5605

This theorem is used by:  weeq12d  5639  oieq1  9510  hartogslem1  9540  wemapwe  9702  infxpenlem  10096  dfac8b  10114  ac10ct  10117  canthnumlem  10737  canthp1lem2  10742  pwfseqlem4a  10750  pwfseqlem4  10751  ltbwe  22359  vitali  25940  dfac15  35810  weexenwe  35813  acwer1prclem  35816  vonf1onprcf1ac  35964  onprcf1acwevdlem1  35965  onprcf1acwevd  35967  prconf1acwevd  35968  numiunnum  37351  fin2so  38624  dnwech  44149  aomclem5  44154  aomclem6  44155  aomclem7  44156