Theorem neli 3054

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

Syntax hints:  ¬ wn 3   ∈ wcel 2108   ∉ wnel 3052

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 3053

This theorem is referenced by:  alephprc  10168  pnfnre2  11332  renepnf  11338  renemnf  11339  ltxrlt  11360  nn0nepnf  12633  xrltnr  13182  pnfnlt  13191  nltmnf  13192  hashclb  14407  hasheq0  14412  egt2lt3  16254  nthruc  16300  pcgcd1  16924  pc2dvds  16926  ramtcl2  17058  nsmndex1  18948  odhash3  19618  xrsmgmdifsgrp  21444  xrsdsreclblem  21453  topnex  23024  pnfnei  23249  mnfnei  23250  zclmncvs  25201  i1f0rn  25736  deg1nn0clb  26149  rgrx0ndm  29629  rgrx0nd  29630  f1resfz0f1d  35081  gonan0  35360  inaex  44266  mnfnre2  45311