Theorem neli 3031

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

Syntax hints:  ¬ wn 3   ∈ wcel 2109   ∉ wnel 3029

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 3030

This theorem is referenced by:  alephprc  9993  pnfnre2  11157  renepnf  11163  renemnf  11164  ltxrlt  11186  nn0nepnf  12465  xrltnr  13021  pnfnlt  13030  nltmnf  13031  hashclb  14265  hasheq0  14270  egt2lt3  16115  nthruc  16161  pcgcd1  16789  pc2dvds  16791  ramtcl2  16923  nsmndex1  18787  odhash3  19455  xrsmgmdifsgrp  21315  xrsdsreclblem  21319  topnex  22881  pnfnei  23105  mnfnei  23106  zclmncvs  25046  i1f0rn  25581  deg1nn0clb  25993  rgrx0ndm  29539  rgrx0nd  29540  trisecnconstr  33765  f1resfz0f1d  35097  gonan0  35375  inaex  44280  mnfnre2  45385  fonex  48861