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

Theorem neli 2802
Description: Inference associated with df-nel 2665. (Contributed by BJ, 7-Jul-2018.)
Hypothesis
Ref Expression
neli.1  |-  A  e/  B
Assertion
Ref Expression
neli  |-  -.  A  e.  B

Proof of Theorem neli
StepHypRef Expression
1 neli.1 . 2  |-  A  e/  B
2 df-nel 2665 . 2  |-  ( A  e/  B  <->  -.  A  e.  B )
31, 2mpbi 208 1  |-  -.  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    e. wcel 1767    e/ wnel 2663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-nel 2665
This theorem is referenced by:  alephprc  8476  renepnf  9637  renemnf  9638  ltxrlt  9651  xrltnr  11326  pnfnlt  11333  nltmnf  11334  hashclb  12394  hasheq0  12397  egt2lt3  13796  nthruc  13841  pcgcd1  14255  pc2dvds  14257  ramtcl2  14384  odhash3  16392  xrsdsreclblem  18232  pnfnei  19487  mnfnei  19488  i1f0rn  21824  deg1nn0clb  22225
  Copyright terms: Public domain W3C validator