Theorem nelir 2900

Description: Inference associated with df-nel 2898. (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

Step	Hyp	Ref	Expression
1		nelir.1	. 2 |- -. A e. B
2		df-nel 2898	. 2 |- ( A e/ B <-> -. A e. B )
3	1, 2	mpbir 221	1 |- A e/ B

Syntax hints:   -. wn 3   e. wcel 1990   e/ wnel 2897

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 197  df-nel 2898

This theorem is referenced by:  ru  3434  prneli  4202  snnexOLD  6967  ruv  8507  ruALT  8508  cardprc  8806  pnfnre  10081  mnfnre  10082  wrdlndm  13321  eirr  14933  sqrt2irr  14979  lcmfnnval  15337  lcmf0  15347  zringndrg  19838  topnex  20800  zfbas  21700  aaliou3  24106  finsumvtxdg2sstep  26445  clwwlksn0  26907  xrge0iifcnv  29979  bj-0nel1  32940  bj-1nel0  32941  bj-0nelsngl  32959  fmtnoinf  41448  fmtno5nprm  41495  0nodd  41810  2nodd  41812  1neven  41932  2zrngnring  41952