Theorem neli 3034

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

Syntax hints:  ¬ wn 3   ∈ wcel 2111   ∉ wnel 3032

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 3033

This theorem is referenced by:  alephprc  9990  pnfnre2  11154  renepnf  11160  renemnf  11161  ltxrlt  11183  nn0nepnf  12462  xrltnr  13018  pnfnlt  13027  nltmnf  13028  hashclb  14265  hasheq0  14270  egt2lt3  16115  nthruc  16161  pcgcd1  16789  pc2dvds  16791  ramtcl2  16923  nsmndex1  18821  odhash3  19488  xrsmgmdifsgrp  21345  xrsdsreclblem  21349  topnex  22911  pnfnei  23135  mnfnei  23136  zclmncvs  25075  i1f0rn  25610  deg1nn0clb  26022  rgrx0ndm  29572  rgrx0nd  29573  trisecnconstr  33805  f1resfz0f1d  35158  gonan0  35436  inaex  44400  mnfnre2  45504  fonex  48977