Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  weeq1 Structured version   Visualization version   GIF version

Theorem weeq1 5131
 Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)
Assertion
Ref Expression
weeq1 (𝑅 = 𝑆 → (𝑅 We 𝐴𝑆 We 𝐴))

Proof of Theorem weeq1
StepHypRef Expression
1 freq1 5113 . . 3 (𝑅 = 𝑆 → (𝑅 Fr 𝐴𝑆 Fr 𝐴))
2 soeq1 5083 . . 3 (𝑅 = 𝑆 → (𝑅 Or 𝐴𝑆 Or 𝐴))
31, 2anbi12d 747 . 2 (𝑅 = 𝑆 → ((𝑅 Fr 𝐴𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴)))
4 df-we 5104 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
5 df-we 5104 . 2 (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴))
63, 4, 53bitr4g 303 1 (𝑅 = 𝑆 → (𝑅 We 𝐴𝑆 We 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   Or wor 5063   Fr wfr 5099   We wwe 5101 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-ex 1745  df-cleq 2644  df-clel 2647  df-ral 2946  df-rex 2947  df-br 4686  df-po 5064  df-so 5065  df-fr 5102  df-we 5104 This theorem is referenced by:  oieq1  8458  hartogslem1  8488  wemapwe  8632  infxpenlem  8874  dfac8b  8892  ac10ct  8895  fpwwe2cbv  9490  fpwwe2lem2  9492  fpwwe2lem5  9494  fpwwecbv  9504  fpwwelem  9505  canthnumlem  9508  canthwelem  9510  canthwe  9511  canthp1lem2  9513  pwfseqlem4a  9521  pwfseqlem4  9522  ltbwe  19520  vitali  23427  fin2so  33526  weeq12d  37927  dnwech  37935  aomclem5  37945  aomclem6  37946  aomclem7  37947
 Copyright terms: Public domain W3C validator