Theorem neli 3040

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

Syntax hints:  ¬ wn 3   ∈ wcel 2119   ∉ wnel 3038

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 208  df-nel 3039

This theorem is referenced by:  alephprc  10012  pnfnre2  11178  renepnf  11184  renemnf  11185  ltxrlt  11207  nn0nepnf  12509  xrltnr  13061  pnfnlt  13070  nltmnf  13071  hashclb  14311  hasheq0  14316  egt2lt3  16164  nthruc  16210  pcgcd1  16839  pc2dvds  16841  ramtcl2  16973  nsmndex1  18875  odhash3  19542  xrsmgmdifsgrp  21384  xrsdsreclblem  21388  topnex  22979  pnfnei  23203  mnfnei  23204  zclmncvs  25133  i1f0rn  25667  deg1nn0clb  26073  rgrx0ndm  29680  rgrx0nd  29681  nowisdomv  30562  ply1coedeg  33672  trisecnconstr  33976  f1resfz0f1d  35342  gonan0  35620  inaex  44741  mnfnre2  45840  fonex  49357