Theorem neli 3048

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

Syntax hints:  ¬ wn 3   ∈ wcel 2106   ∉ wnel 3046

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 206  df-nel 3047

This theorem is referenced by:  alephprc  10096  pnfnre2  11258  renepnf  11264  renemnf  11265  ltxrlt  11286  nn0nepnf  12554  xrltnr  13101  pnfnlt  13110  nltmnf  13111  hashclb  14320  hasheq0  14325  egt2lt3  16151  nthruc  16197  pcgcd1  16812  pc2dvds  16814  ramtcl2  16946  nsmndex1  18796  odhash3  19446  xrsmgmdifsgrp  20988  xrsdsreclblem  20997  topnex  22506  pnfnei  22731  mnfnei  22732  zclmncvs  24672  i1f0rn  25206  deg1nn0clb  25615  rgrx0ndm  28888  rgrx0nd  28889  f1resfz0f1d  34172  gonan0  34452  inaex  43144  mnfnre2  44191