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

Theorem neli 2767
Description: Inference associated with df-nel 2628. (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 2628 . 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 1870    e/ wnel 2626
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 2628
This theorem is referenced by:  alephprc  8528  renepnf  9687  renemnf  9688  ltxrlt  9703  xrltnr  11421  pnfnlt  11430  nltmnf  11431  hashclb  12537  hasheq0  12541  egt2lt3  14236  nthruc  14281  pcgcd1  14780  pc2dvds  14782  ramtcl2  14920  ramtcl2OLD  14921  odhash3  17154  xrsmgmdifsgrp  18931  xrsdsreclblem  18940  pnfnei  20158  mnfnei  20159  i1f0rn  22508  deg1nn0clb  22907
  Copyright terms: Public domain W3C validator