Theorem weeq1 5638

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 5618	. . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴))
2		soeq1 5580	. . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴))
3	1, 2	anbi12d 644	. 2 ⊢ (𝑅 = 𝑆 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴)))
4		df-we 5606	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
5		df-we 5606	. 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 5558   Fr wfr 5601   We wwe 5603

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-ex 1813  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-br 5104  df-po 5559  df-so 5560  df-fr 5604  df-we 5606

This theorem is used by:  weeq12d  5640  oieq1  9499  hartogslem1  9529  wemapwe  9691  infxpenlem  10085  dfac8b  10103  ac10ct  10106  canthnumlem  10726  canthp1lem2  10731  pwfseqlem4a  10739  pwfseqlem4  10740  ltbwe  22346  vitali  25927  numiunnum  37238  fin2so  38510  dnwech  44034  aomclem5  44044  aomclem6  44045  aomclem7  44046