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

Theorem weeq2 5238
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 5220 . . 3 (𝐴 = 𝐵 → (𝑅 Fr 𝐴𝑅 Fr 𝐵))
2 soeq2 5190 . . 3 (𝐴 = 𝐵 → (𝑅 Or 𝐴𝑅 Or 𝐵))
31, 2anbi12d 608 . 2 (𝐴 = 𝐵 → ((𝑅 Fr 𝐴𝑅 Or 𝐴) ↔ (𝑅 Fr 𝐵𝑅 Or 𝐵)))
4 df-we 5210 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
5 df-we 5210 . 2 (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵𝑅 Or 𝐵))
63, 4, 53bitr4g 303 1 (𝐴 = 𝐵 → (𝑅 We 𝐴𝑅 We 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1630   Or wor 5169   Fr wfr 5205   We wwe 5207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-ral 3065  df-in 3728  df-ss 3735  df-po 5170  df-so 5171  df-fr 5208  df-we 5210
This theorem is referenced by:  ordeq  5873  0we1  7739  oieq2  8573  hartogslem1  8602  wemapwe  8757  ween  9057  dfac8  9158  weth  9518  fpwwe2cbv  9653  fpwwe2lem2  9655  fpwwe2lem5  9657  fpwwecbv  9667  fpwwelem  9668  canthwelem  9673  canthwe  9674  pwfseqlem4a  9684  pwfseqlem4  9685  ltweuz  12967  ltwenn  12968  bpolylem  14984  ltbwe  19686  vitali  23600  weeq12d  38129  aomclem6  38148  omeiunle  41245
  Copyright terms: Public domain W3C validator