Theorem weeq1 5645

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 5625	. . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴))
2		soeq1 5587	. . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴))
3	1, 2	anbi12d 644	. 2 ⊢ (𝑅 = 𝑆 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴)))
4		df-we 5613	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
5		df-we 5613	. 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 1570   Or wor 5565   Fr wfr 5608   We wwe 5610

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-ex 1813  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-br 5109  df-po 5566  df-so 5567  df-fr 5611  df-we 5613

This theorem is used by:  weeq12d  5647  oieq1  9543  hartogslem1  9573  wemapwe  9735  infxpenlem  10131  dfac8b  10149  ac10ct  10152  canthnumlem  10772  canthp1lem2  10777  pwfseqlem4a  10785  pwfseqlem4  10786  ltbwe  22408  vitali  25989  dfac15  35886  weexenwe  35889  acwer1prclem  35892  vonf1onprcf1ac  36085  onprcf1acwevdlem1  36086  onprcf1acwevd  36088  prconf1acwevd  36089  numiunnum  37473  fin2so  38798  dnwech  44321  aomclem5  44326  aomclem6  44327  aomclem7  44328