Theorem neli 2899

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

Step	Hyp	Ref	Expression
1		neli.1	. 2 |- A e/ B
2		df-nel 2898	. 2 |- ( A e/ B <-> -. A e. B )
3	1, 2	mpbi 220	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:  alephprc  8922  renepnf  10087  renemnf  10088  ltxrlt  10108  nn0nepnf  11371  xrltnr  11953  pnfnlt  11962  nltmnf  11963  hashclb  13149  hasheq0  13154  egt2lt3  14934  nthruc  14981  pcgcd1  15581  pc2dvds  15583  ramtcl2  15715  odhash3  17991  xrsmgmdifsgrp  19783  xrsdsreclblem  19792  topnex  20800  pnfnei  21024  mnfnei  21025  zclmncvs  22948  i1f0rn  23449  deg1nn0clb  23850  rgrx0ndm  26489  rgrx0nd  26490  mnfnre2  39619  pnfnre2  39628