Theorem neli 3039

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

Syntax hints:  ¬ wn 3   ∈ wcel 2114   ∉ wnel 3037

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 3038

This theorem is referenced by:  alephprc  10021  pnfnre2  11186  renepnf  11192  renemnf  11193  ltxrlt  11215  nn0nepnf  12494  xrltnr  13045  pnfnlt  13054  nltmnf  13055  hashclb  14293  hasheq0  14298  egt2lt3  16143  nthruc  16189  pcgcd1  16817  pc2dvds  16819  ramtcl2  16951  nsmndex1  18850  odhash3  19517  xrsmgmdifsgrp  21375  xrsdsreclblem  21379  topnex  22952  pnfnei  23176  mnfnei  23177  zclmncvs  25116  i1f0rn  25651  deg1nn0clb  26063  rgrx0ndm  29679  rgrx0nd  29680  nowisdomv  30561  ply1coedeg  33682  trisecnconstr  33970  f1resfz0f1d  35330  gonan0  35608  inaex  44653  mnfnre2  45754  fonex  49226