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

Theorem weeq2 5093
Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
weeq2 (𝐴 = 𝐵 → (𝑅 We 𝐴𝑅 We 𝐵))

Proof of Theorem weeq2
StepHypRef Expression
1 freq2 5075 . . 3 (𝐴 = 𝐵 → (𝑅 Fr 𝐴𝑅 Fr 𝐵))
2 soeq2 5045 . . 3 (𝐴 = 𝐵 → (𝑅 Or 𝐴𝑅 Or 𝐵))
31, 2anbi12d 746 . 2 (𝐴 = 𝐵 → ((𝑅 Fr 𝐴𝑅 Or 𝐴) ↔ (𝑅 Fr 𝐵𝑅 Or 𝐵)))
4 df-we 5065 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
5 df-we 5065 . 2 (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵𝑅 Or 𝐵))
63, 4, 53bitr4g 303 1 (𝐴 = 𝐵 → (𝑅 We 𝐴𝑅 We 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481   Or wor 5024   Fr wfr 5060   We wwe 5062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-ral 2914  df-in 3574  df-ss 3581  df-po 5025  df-so 5026  df-fr 5063  df-we 5065
This theorem is referenced by:  ordeq  5718  0we1  7571  oieq2  8403  hartogslem1  8432  wemapwe  8579  ween  8843  dfac8  8942  weth  9302  fpwwe2cbv  9437  fpwwe2lem2  9439  fpwwe2lem5  9441  fpwwecbv  9451  fpwwelem  9452  canthwelem  9457  canthwe  9458  pwfseqlem4a  9468  pwfseqlem4  9469  ltweuz  12743  ltwenn  12744  bpolylem  14760  ltbwe  19453  vitali  23363  weeq12d  37429  aomclem6  37448  omeiunle  40494
  Copyright terms: Public domain W3C validator