Theorem neli 2789

Description: Inference associated with df-nel 2687. (Contributed by BJ, 7-Jul-2018.)

Hypothesis

Ref	Expression
neli.1	⊢ 𝐴 ∉ 𝐵

Assertion

Ref	Expression
neli	⊢ ¬ 𝐴 ∈ 𝐵

Proof of Theorem neli

Step	Hyp	Ref	Expression
1		neli.1	. 2 ⊢ 𝐴 ∉ 𝐵
2		df-nel 2687	. 2 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
3	1, 2	mpbi 218	1 ⊢ ¬ 𝐴 ∈ 𝐵

Syntax hints:  ¬ wn 3   ∈ wcel 1938   ∉ wnel 2685

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 195  df-nel 2687

This theorem is referenced by:  alephprc  8681  renepnf  9842  renemnf  9843  ltxrlt  9858  xrltnr  11700  pnfnlt  11709  nltmnf  11710  hashclb  12876  hasheq0  12880  egt2lt3  14642  nthruc  14688  pcgcd1  15303  pc2dvds  15305  ramtcl2  15437  odhash3  17719  xrsmgmdifsgrp  19506  xrsdsreclblem  19515  pnfnei  20737  mnfnei  20738  i1f0rn  23130  deg1nn0clb  23529  bj-topnex  32078  nn0nepnf  40311  rgrx0ndm  40898  rgrx0nd  40899