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

Theorem neli 2783
Description: Inference associated with df-nel 2647. (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 2647 . 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 1758    e/ wnel 2645
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 2647
This theorem is referenced by:  alephprc  8372  renepnf  9534  renemnf  9535  ltxrlt  9548  xrltnr  11204  pnfnlt  11211  nltmnf  11212  hashclb  12231  hasheq0  12234  egt2lt3  13592  nthruc  13637  pcgcd1  14047  pc2dvds  14049  ramtcl2  14176  odhash3  16181  xrsdsreclblem  17970  pnfnei  18942  mnfnei  18943  i1f0rn  21278  deg1nn0clb  21679
  Copyright terms: Public domain W3C validator