MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sonr Unicode version

Theorem sonr 4438
Description: A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
Assertion
Ref Expression
sonr  |-  ( ( R  Or  A  /\  B  e.  A )  ->  -.  B R B )

Proof of Theorem sonr
StepHypRef Expression
1 sopo 4434 . 2  |-  ( R  Or  A  ->  R  Po  A )
2 poirr 4428 . 2  |-  ( ( R  Po  A  /\  B  e.  A )  ->  -.  B R B )
31, 2sylan 457 1  |-  ( ( R  Or  A  /\  B  e.  A )  ->  -.  B R B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    e. wcel 1715   class class class wbr 4125    Po wpo 4415    Or wor 4416
This theorem is referenced by:  sotric  4443  sotrieq  4444  soirri  5172  soirriOLD  5177  suppr  7366  hartogslem1  7404  canth4  8416  canthwelem  8419  pwfseqlem4  8431  1ne0sr  8865  ltnr  9062  opsrtoslem2  16436  sltirr  25065
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ral 2633  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-br 4126  df-po 4417  df-so 4418
  Copyright terms: Public domain W3C validator