Theorem neli 3036

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

Syntax hints:  ¬ wn 3   ∈ wcel 2113   ∉ wnel 3034

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 3035

This theorem is referenced by:  alephprc  10007  pnfnre2  11172  renepnf  11178  renemnf  11179  ltxrlt  11201  nn0nepnf  12480  xrltnr  13031  pnfnlt  13040  nltmnf  13041  hashclb  14279  hasheq0  14284  egt2lt3  16129  nthruc  16175  pcgcd1  16803  pc2dvds  16805  ramtcl2  16937  nsmndex1  18836  odhash3  19503  xrsmgmdifsgrp  21361  xrsdsreclblem  21365  topnex  22938  pnfnei  23162  mnfnei  23163  zclmncvs  25102  i1f0rn  25637  deg1nn0clb  26049  rgrx0ndm  29616  rgrx0nd  29617  ply1coedeg  33619  trisecnconstr  33898  f1resfz0f1d  35257  gonan0  35535  inaex  44480  mnfnre2  45582  fonex  49054