Theorem neli 3072

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

Syntax hints:  ¬ wn 3   ∈ wcel 2149   ∉ wnel 3070

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 3071

This theorem is referenced by:  alephprc  10083  pnfnre2  11251  renepnf  11257  renemnf  11258  ltxrlt  11280  nn0nepnf  12585  xrltnr  13144  pnfnlt  13153  nltmnf  13154  hashclb  14394  hasheq0  14399  egt2lt3  16262  nthruc  16308  pcgcd1  16937  pc2dvds  16939  ramtcl2  17071  nsmndex1  18975  odhash3  19646  xrsmgmdifsgrp  21528  xrsdsreclblem  21532  topnex  23122  pnfnei  23346  mnfnei  23347  zclmncvs  25276  i1f0rn  25810  deg1nn0clb  26216  rgrx0ndm  29884  rgrx0nd  29885  nowisdomv  30766  ply1coedeg  33824  trisecnconstr  34127  f1resfz0f1d  35538  gonan0  35817  inaex  44933  mnfnre2  46037  fonex  49564