Theorem neli 3066

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

Syntax hints:  ¬ wn 3   ∈ wcel 2143   ∉ wnel 3064

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 210  df-nel 3065

This theorem is referenced by:  alephprc  10079  pnfnre2  11246  renepnf  11252  renemnf  11253  ltxrlt  11275  nn0nepnf  12580  xrltnr  13139  pnfnlt  13148  nltmnf  13149  hashclb  14390  hasheq0  14395  egt2lt3  16257  nthruc  16303  pcgcd1  16932  pc2dvds  16934  ramtcl2  17066  nsmndex1  18970  odhash3  19641  xrsmgmdifsgrp  21559  xrsdsreclblem  21563  topnex  23153  pnfnei  23377  mnfnei  23378  zclmncvs  25307  i1f0rn  25841  deg1nn0clb  26247  rgrx0ndm  29943  rgrx0nd  29944  nowisdomv  30825  ply1coedeg  33879  trisecnconstr  34182  f1resfz0f1d  35605  gonan0  35884  inaex  45027  mnfnre2  46131  nthrucw  47627  fonex  49665