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

Theorem neli 2756
Description: Inference associated with df-nel 2617. (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 2617 . 2  |-  ( A  e/  B  <->  -.  A  e.  B )
31, 2mpbi 211 1  |-  -.  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    e. wcel 1872    e/ wnel 2615
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 188  df-nel 2617
This theorem is referenced by:  alephprc  8537  renepnf  9695  renemnf  9696  ltxrlt  9711  xrltnr  11428  pnfnlt  11437  nltmnf  11438  hashclb  12546  hasheq0  12550  egt2lt3  14257  nthruc  14302  pcgcd1  14825  pc2dvds  14827  ramtcl2  14965  ramtcl2OLD  14966  odhash3  17224  xrsmgmdifsgrp  19004  xrsdsreclblem  19013  pnfnei  20234  mnfnei  20235  i1f0rn  22638  deg1nn0clb  23037
  Copyright terms: Public domain W3C validator