Theorem neli 3038

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

Syntax hints:  ¬ wn 3   ∈ wcel 2140   ∉ wnel 3036

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 3037

This theorem is referenced by:  alephprc  9133  renepnf  10300  renemnf  10301  ltxrlt  10321  nn0nepnf  11584  xrltnr  12167  pnfnlt  12176  nltmnf  12177  hashclb  13362  hasheq0  13367  egt2lt3  15154  nthruc  15201  pcgcd1  15804  pc2dvds  15806  ramtcl2  15938  odhash3  18212  xrsmgmdifsgrp  20006  xrsdsreclblem  20015  topnex  21023  pnfnei  21247  mnfnei  21248  zclmncvs  23169  i1f0rn  23669  deg1nn0clb  24070  rgrx0ndm  26721  rgrx0nd  26722  mnfnre2  40136  pnfnre2  40145