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 2114   ∉ 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  10021  pnfnre2  11187  renepnf  11193  renemnf  11194  ltxrlt  11216  nn0nepnf  12518  xrltnr  13070  pnfnlt  13079  nltmnf  13080  hashclb  14320  hasheq0  14325  egt2lt3  16173  nthruc  16219  pcgcd1  16848  pc2dvds  16850  ramtcl2  16982  nsmndex1  18884  odhash3  19551  xrsmgmdifsgrp  21389  xrsdsreclblem  21393  topnex  22961  pnfnei  23185  mnfnei  23186  zclmncvs  25115  i1f0rn  25649  deg1nn0clb  26055  rgrx0ndm  29662  rgrx0nd  29663  nowisdomv  30544  ply1coedeg  33649  trisecnconstr  33936  f1resfz0f1d  35296  gonan0  35574  inaex  44724  mnfnre2  45825  fonex  49342