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

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

Proof of Theorem nelir
StepHypRef Expression
1 nelir.1 . 2  |-  -.  A  e.  B
2 df-nel 2652 . 2  |-  ( A  e/  B  <->  -.  A  e.  B )
31, 2mpbir 209 1  |-  A  e/  B
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    e. wcel 1823    e/ wnel 2650
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 2652
This theorem is referenced by:  ru  3323  snnex  6579  ruv  8018  ruALT  8019  cardprc  8352  pnfnre  9624  mnfnre  9625  eirr  14023  sqrt2irr  14069  zfbas  20566  aaliou3  22916  xrge0iifcnv  28153  0nodd  32889  2nodd  32891  1neven  33011  2zrngnring  33031  AnelBC  33567  bj-0nel1  34929  bj-1nel0  34930  bj-0nelsngl  34949
  Copyright terms: Public domain W3C validator