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 230	1 ⊢ ¬ 𝐴 ∈ 𝐵

Syntax hints:  ¬ wn 3   ∈ wcel 2108   ∉ 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 207  df-nel 3047

This theorem is referenced by:  alephprc  10139  pnfnre2  11303  renepnf  11309  renemnf  11310  ltxrlt  11331  nn0nepnf  12607  xrltnr  13161  pnfnlt  13170  nltmnf  13171  hashclb  14397  hasheq0  14402  egt2lt3  16242  nthruc  16288  pcgcd1  16915  pc2dvds  16917  ramtcl2  17049  nsmndex1  18926  odhash3  19594  xrsmgmdifsgrp  21421  xrsdsreclblem  21430  topnex  23003  pnfnei  23228  mnfnei  23229  zclmncvs  25182  i1f0rn  25717  deg1nn0clb  26129  rgrx0ndm  29611  rgrx0nd  29612  f1resfz0f1d  35119  gonan0  35397  inaex  44316  mnfnre2  45407