Theorem neli 3039

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

Syntax hints:  ¬ wn 3   ∈ wcel 2114   ∉ wnel 3037

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 207  df-nel 3038

This theorem is referenced by:  alephprc  10015  pnfnre2  11181  renepnf  11187  renemnf  11188  ltxrlt  11210  nn0nepnf  12512  xrltnr  13064  pnfnlt  13073  nltmnf  13074  hashclb  14314  hasheq0  14319  egt2lt3  16167  nthruc  16213  pcgcd1  16842  pc2dvds  16844  ramtcl2  16976  nsmndex1  18878  odhash3  19545  xrsmgmdifsgrp  21401  xrsdsreclblem  21405  topnex  22974  pnfnei  23198  mnfnei  23199  zclmncvs  25128  i1f0rn  25662  deg1nn0clb  26068  rgrx0ndm  29680  rgrx0nd  29681  nowisdomv  30562  ply1coedeg  33667  trisecnconstr  33955  f1resfz0f1d  35315  gonan0  35593  inaex  44745  mnfnre2  45846  fonex  49357