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

Theorem domnsym 9138
Description: Theorem 22(i) of [Suppes] p. 97. (Contributed by NM, 10-Jun-1998.)
Assertion
Ref Expression
domnsym (𝐴𝐵 → ¬ 𝐵𝐴)

Proof of Theorem domnsym
StepHypRef Expression
1 brdom2 9021 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
2 sdomnsym 9137 . . 3 (𝐴𝐵 → ¬ 𝐵𝐴)
3 sdomnen 9020 . . . 4 (𝐵𝐴 → ¬ 𝐵𝐴)
4 ensym 9042 . . . 4 (𝐴𝐵𝐵𝐴)
53, 4nsyl3 138 . . 3 (𝐴𝐵 → ¬ 𝐵𝐴)
62, 5jaoi 857 . 2 ((𝐴𝐵𝐴𝐵) → ¬ 𝐵𝐴)
71, 6sylbi 217 1 (𝐴𝐵 → ¬ 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 847   class class class wbr 5148  cen 8981  cdom 8982  csdm 8983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987
This theorem is referenced by:  sdom0OLD  9148  sdomdomtr  9149  domsdomtr  9151  sdomdif  9164  onsdominel  9165  nndomogOLD  9261  sdom1OLD  9277  fofinf1o  9370  carddom2  10015  fidomtri  10031  fidomtri2  10032  infxpenlem  10051  alephordi  10112  infdif  10246  infdif2  10247  cfslbn  10305  cfslb2n  10306  fincssdom  10361  fin45  10430  domtriom  10481  alephval2  10610  alephreg  10620  pwcfsdom  10621  cfpwsdom  10622  pwfseqlem3  10698  gchpwdom  10708  gchaleph  10709  hargch  10711  gchhar  10717  winainflem  10731  rankcf  10815  tskcard  10819  vdwlem12  17026  odinf  19596  rectbntr0  24868  erdszelem10  35185  finminlem  36301  fimgmcyc  42521  fphpd  42804
  Copyright terms: Public domain W3C validator