Theorem neli 3076

Description: Inference associated with df-nel 3075. (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 3075	. 2 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
3	1, 2	mpbi 222	1 ⊢ ¬ 𝐴 ∈ 𝐵

Syntax hints:  ¬ wn 3   ∈ wcel 2157   ∉ wnel 3074

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 199  df-nel 3075

This theorem is referenced by:  alephprc  9208  renepnf  10376  renemnf  10377  ltxrlt  10398  nn0nepnf  11660  xrltnr  12200  pnfnlt  12209  nltmnf  12210  hashclb  13399  hasheq0  13404  egt2lt3  15270  nthruc  15317  pcgcd1  15914  pc2dvds  15916  ramtcl2  16048  odhash3  18304  xrsmgmdifsgrp  20105  xrsdsreclblem  20114  topnex  21129  pnfnei  21353  mnfnei  21354  zclmncvs  23275  i1f0rn  23790  deg1nn0clb  24191  rgrx0ndm  26843  rgrx0nd  26844  mnfnre2  40362  pnfnre2  40371