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 230	1 ⊢ ¬ 𝐴 ∈ 𝐵

Syntax hints:  ¬ wn 3   ∈ wcel 2113   ∉ 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 207  df-nel 3037

This theorem is referenced by:  alephprc  10009  pnfnre2  11174  renepnf  11180  renemnf  11181  ltxrlt  11203  nn0nepnf  12482  xrltnr  13033  pnfnlt  13042  nltmnf  13043  hashclb  14281  hasheq0  14286  egt2lt3  16131  nthruc  16177  pcgcd1  16805  pc2dvds  16807  ramtcl2  16939  nsmndex1  18838  odhash3  19505  xrsmgmdifsgrp  21363  xrsdsreclblem  21367  topnex  22940  pnfnei  23164  mnfnei  23165  zclmncvs  25104  i1f0rn  25639  deg1nn0clb  26051  rgrx0ndm  29667  rgrx0nd  29668  ply1coedeg  33670  trisecnconstr  33949  f1resfz0f1d  35308  gonan0  35586  inaex  44548  mnfnre2  45650  fonex  49122